The derivative ideal of a polynomial ideal is generated by the partial derivatives

[Kol07, Definition 73]: "D(f₁, …, f_s) = (fᵢ, ∂fᵢ/∂xⱼ)". On a polynomial ring R[X_i : i ∈ σ] every R-derivation is the R[X]-combination ∑ δ(X_i) ∂_i of Mathlib's partial derivatives MvPolynomial.pderiv (derivation_mem_span_range_pderiv, by derivation_ext), so Ideal.derivative_span_eq_of_span of Hironaka.Derivative gives D(⟨S⟩) = ⟨S, ∂_i s⟩ (derivative_span_pderiv). Ideal.mem_of_C_mul_mem divides a generator by a nonzero scalar of the field. These are the tools of the worked examples of this directory.

theorem MvPolynomial.derivation_mem_span_range_pderiv {σ : Type u_1} {R : Type u_2} [Finite σ] [CommRing R] (δ : Derivation R (MvPolynomial σ R) (MvPolynomial σ R)) : δ ∈ Submodule.span (MvPolynomial σ R) (Set.range pderiv)

Every R-derivation of R[X_i] into itself is ∑ᵢ δ(X_i) • ∂ᵢ (the derivations ∂/∂x_j generate, [Kol07, Definition 73]).

theorem MvPolynomial.derivative_span_pderiv {σ : Type u_1} {R : Type u_2} [Finite σ] [CommRing R] (S : Set (MvPolynomial σ R)) : Ideal.derivative R (Ideal.span S) = Ideal.span (S ∪ ⋃ (i : σ), ⇑(pderiv i) '' S)

D(⟨S⟩) = ⟨S, ∂ᵢ s : s ∈ S⟩ on a polynomial ring [Kol07, Definition 73].

theorem Ideal.mem_of_algebraMap_mul_mem {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] {J : Ideal A} {q : K} (hq : q ≠ 0) {a : A} (h : (algebraMap K A) q * a ∈ J) : a ∈ J

Dividing a member of an ideal by a nonzero scalar: if q • a ∈ J with q ≠ 0 in the field K, then a ∈ J.

theorem MvPolynomial.mem_of_C_mul_mem {σ : Type u_1} {K : Type u_2} [Field K] {J : Ideal (MvPolynomial σ K)} {q : K} (hq : q ≠ 0) {a : MvPolynomial σ K} (h : C q * a ∈ J) : a ∈ J

Ideal.mem_of_algebraMap_mul_mem for MvPolynomial.C.