# Documentation

Mathlib.Data.MvPolynomial.Derivation

# Derivations of multivariate polynomials #

In this file we prove that a derivation of MvPolynomial σ R is determined by its values on all monomials MvPolynomial.X i. We also provide a constructor MvPolynomial.mkDerivation that builds a derivation from its values on X is and a linear equivalence MvPolynomial.mkDerivationEquiv between σ → A and Derivation (MvPolynomial σ R) A.

def MvPolynomial.mkDerivationₗ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [] [] [Module R A] [Module () A] (f : σA) :

The derivation on MvPolynomial σ R that takes value f i on X i, as a linear map. Use MvPolynomial.mkDerivation instead.

Instances For
theorem MvPolynomial.mkDerivationₗ_monomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] (f : σA) (s : σ →₀ ) (r : R) :
↑() (↑() r) = r Finsupp.sum s fun i k => ↑(MvPolynomial.monomial (s - fun₀ | i => 1)) k f i
theorem MvPolynomial.mkDerivationₗ_C {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] (f : σA) (r : R) :
↑() (MvPolynomial.C r) = 0
theorem MvPolynomial.mkDerivationₗ_X {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] (f : σA) (i : σ) :
↑() () = f i
@[simp]
theorem MvPolynomial.derivation_C {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] (D : Derivation R () A) (a : R) :
D (MvPolynomial.C a) = 0
@[simp]
theorem MvPolynomial.derivation_C_mul {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] (D : Derivation R () A) (a : R) (f : ) :
MvPolynomial.C a D f = a D f
theorem MvPolynomial.derivation_eqOn_supported {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] {D₁ : Derivation R () A} {D₂ : Derivation R () A} {s : Set σ} (h : Set.EqOn (D₁ MvPolynomial.X) (D₂ MvPolynomial.X) s) {f : } (hf : ) :
D₁ f = D₂ f

If two derivations agree on X i, i ∈ s, then they agree on all polynomials from MvPolynomial.supported R s.

theorem MvPolynomial.derivation_eq_of_forall_mem_vars {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] {D₁ : Derivation R () A} {D₂ : Derivation R () A} {f : } (h : ∀ (i : σ), D₁ () = D₂ ()) :
D₁ f = D₂ f
theorem MvPolynomial.derivation_eq_zero_of_forall_mem_vars {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] {D : Derivation R () A} {f : } (h : ∀ (i : σ), D () = 0) :
D f = 0
theorem MvPolynomial.derivation_ext {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] {D₁ : Derivation R () A} {D₂ : Derivation R () A} (h : ∀ (i : σ), D₁ () = D₂ ()) :
D₁ = D₂
theorem MvPolynomial.leibniz_iff_X {σ : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (D : →ₗ[R] A) (h₁ : D 1 = 0) :
(∀ (p q : ), D (p * q) = p D q + q D p) ∀ (s : σ →₀ ) (i : σ), D (↑() 1 * ) = ↑() 1 D () + D (↑() 1)
def MvPolynomial.mkDerivation {σ : Type u_1} (R : Type u_2) {A : Type u_3} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (f : σA) :
Derivation R () A

The derivation on MvPolynomial σ R that takes value f i on X i.

Instances For
@[simp]
theorem MvPolynomial.mkDerivation_X {σ : Type u_1} (R : Type u_2) {A : Type u_3} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (f : σA) (i : σ) :
↑() () = f i
theorem MvPolynomial.mkDerivation_monomial {σ : Type u_1} (R : Type u_2) {A : Type u_3} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (f : σA) (s : σ →₀ ) (r : R) :
↑() (↑() r) = r Finsupp.sum s fun i k => ↑(MvPolynomial.monomial (s - fun₀ | i => 1)) k f i
def MvPolynomial.mkDerivationEquiv {σ : Type u_1} (R : Type u_2) {A : Type u_3} [] [] [Module R A] [Module () A] [IsScalarTower R () A] :
(σA) ≃ₗ[R] Derivation R () A

MvPolynomial.mkDerivation as a linear equivalence.

Instances For