# 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} [] (a : ) :
Polynomial.derivative' a = Polynomial.derivative a
def Polynomial.derivative' {R : Type u_1} [] :
Derivation R () ()

Polynomial.derivative as a derivation.

Instances For
@[simp]
theorem Polynomial.derivation_C {R : Type u_1} {A : Type u_2} [] [] [Module R A] [Module () A] (D : Derivation R () A) (a : R) :
D (Polynomial.C a) = 0
@[simp]
theorem Polynomial.C_smul_derivation_apply {R : Type u_1} {A : Type u_2} [] [] [Module R A] [Module () A] (D : Derivation R () A) (a : R) (f : ) :
Polynomial.C a D f = a D f
theorem Polynomial.derivation_ext {R : Type u_1} {A : Type u_2} [] [] [Module R A] [Module () A] {D₁ : Derivation R () A} {D₂ : Derivation R () A} (h : D₁ Polynomial.X = D₂ Polynomial.X) :
D₁ = D₂
def Polynomial.mkDerivation (R : Type u_1) {A : Type u_2} [] [] [Module R A] [Module () A] [IsScalarTower R () A] :

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} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (a : A) (f : ) :
↑(↑() a) f = Polynomial.derivative f a
@[simp]
theorem Polynomial.mkDerivation_X (R : Type u_1) {A : Type u_2} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (a : A) :
↑(↑() a) Polynomial.X = a
theorem Polynomial.mkDerivation_one_eq_derivative' (R : Type u_1) [] :
↑() 1 = Polynomial.derivative'
theorem Polynomial.mkDerivation_one_eq_derivative (R : Type u_1) [] (f : ) :
↑(↑() 1) f = Polynomial.derivative f
def Polynomial.mkDerivationEquiv (R : Type u_1) {A : Type u_2} [] [] [Module R A] [Module () A] [IsScalarTower R () A] :

Polynomial.mkDerivation as a linear equivalence.

Instances For
@[simp]
theorem Polynomial.mkDerivationEquiv_apply (R : Type u_1) {A : Type u_2} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (a : A) :
= ↑() a
@[simp]
theorem Polynomial.mkDerivationEquiv_symm_apply (R : Type u_1) {A : Type u_2} [] [] [Module R A] [Module () A] [IsScalarTower R () A] (D : Derivation R () A) :
= D Polynomial.X