# 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

def
Polynomial.derivative'
{R : Type u_1}
[CommSemiring R]
:

Derivation R (Polynomial R) (Polynomial R)

`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)
:

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₂

def
Polynomial.mkDerivation
(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 →ₗ[R] Derivation R (Polynomial 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}
[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

def
Polynomial.mkDerivationEquiv
(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 ≃ₗ[R] Derivation R (Polynomial R) A

`Polynomial.mkDerivation`

as a linear equivalence.

## Instances For

@[simp]

theorem
Polynomial.mkDerivationEquiv_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)
:

↑(Polynomial.mkDerivationEquiv R) a = ↑(Polynomial.mkDerivation R) a

@[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)
:

↑(LinearEquiv.symm (Polynomial.mkDerivationEquiv R)) D = ↑D Polynomial.X