Documentation

Mathlib.Data.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'_toFun {R : Type u_1} [CommSemiring R] (a : Polynomial R) :
Polynomial.derivative' a = Polynomial.derivative a

Polynomial.derivative as a derivation.

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 {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.

    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] :
      ↑(Polynomial.mkDerivation R) 1 = Polynomial.derivative'
      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.

      Instances For
        @[simp]