Documentation

Mathlib.Algebra.Polynomial.Derivation

Derivations of univariate polynomials #

In this file we prove that an R-derivation of Polynomial R is determined by its value on X. We also provide a constructor Polynomial.mkDerivation that builds a derivation from its value on X, and a linear equivalence Polynomial.mkDerivationEquiv between A and Derivation (Polynomial R) A.

@[simp]
theorem Polynomial.derivative'_apply {R : Type u_1} [CommSemiring R] (a : Polynomial R) :
Polynomial.derivative' a = Polynomial.derivative a

Polynomial.derivative as a derivation.

Equations
  • Polynomial.derivative' = { toFun := Polynomial.derivative, map_add' := , map_smul' := , map_one_eq_zero' := , leibniz' := }
Instances For
    @[simp]
    theorem Polynomial.derivation_C {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R) :
    D (Polynomial.C a) = 0
    @[simp]
    theorem Polynomial.C_smul_derivation_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] (D : Derivation R (Polynomial R) A) (a : R) (f : Polynomial R) :
    Polynomial.C a D f = a D f
    theorem Polynomial.derivation_ext_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] {D₁ : Derivation R (Polynomial R) A} {D₂ : Derivation R (Polynomial R) A} :
    D₁ = D₂ D₁ Polynomial.X = D₂ Polynomial.X
    theorem Polynomial.derivation_ext {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] {D₁ : Derivation R (Polynomial R) A} {D₂ : Derivation R (Polynomial R) A} (h : D₁ Polynomial.X = D₂ Polynomial.X) :
    D₁ = D₂

    The derivation on R[X] that takes the value a on X.

    Equations
    Instances For
      theorem Polynomial.mkDerivation_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) (f : Polynomial R) :
      ((Polynomial.mkDerivation R) a) f = Polynomial.derivative f a
      @[simp]
      theorem Polynomial.mkDerivation_X (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) :
      ((Polynomial.mkDerivation R) a) Polynomial.X = a
      theorem Polynomial.mkDerivation_one_eq_derivative (R : Type u_1) [CommSemiring R] (f : Polynomial R) :
      ((Polynomial.mkDerivation R) 1) f = Polynomial.derivative f

      Polynomial.mkDerivation as a linear equivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Polynomial.mkDerivationEquiv_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (D : Derivation R (Polynomial R) A) :
        (Polynomial.mkDerivationEquiv R).symm D = D Polynomial.X
        @[simp]
        theorem Derivation.compAEval_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (d : Derivation R A M) (a : A) (f : Polynomial R) :
        (d.compAEval a) f = (Module.AEval.of R M a) (d ((Polynomial.aeval a) f))
        def Derivation.compAEval {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (d : Derivation R A M) (a : A) :

        For a derivation d : A → M and an element a : A, d.compAEval a is the derivation of R[X] which takes a polynomial f to d(aeval a f).

        This derivation takes values in Module.AEval R M a, which is M, regarded as an R[X]-module, with the action of a polynomial f defined by f • m = (aeval a f) • m.

        Equations
        Instances For
          theorem Derivation.compAEval_eq {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) :
          (d.compAEval a) f = Polynomial.derivative f (Module.AEval.of R M a) (d a)

          A form of the chain rule: if f is a polynomial over R and d : A → M is an R-derivation then for all a : A we have $$ d(f(a)) = f' (a) d a. $$ The equation is in the R[X]-module Module.AEval R M a. For the same equation in M, see Derivation.compAEval_eq.

          theorem Derivation.comp_aeval_eq {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) :
          d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) d a

          A form of the chain rule: if f is a polynomial over R and d : A → M is an R-derivation then for all a : A we have $$ d(f(a)) = f' (a) d a. $$ The equation is in M. For the same equation in Module.AEval R M a, see Derivation.compAEval_eq.