# 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`

.

`Polynomial.derivative`

as a derivation.

## Equations

- Polynomial.derivative' = { toFun := ⇑Polynomial.derivative, map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

## Instances For

The derivation on `R[X]`

that takes the value `a`

on `X`

.

## Equations

- Polynomial.mkDerivation R = { toFun := fun (a : A) => (LinearMap.toSpanSingleton (Polynomial R) A a).compDer Polynomial.derivative', map_add' := ⋯, map_smul' := ⋯ }

## Instances For

`Polynomial.mkDerivation`

as a linear equivalence.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

- d.compAEval a = { toFun := fun (f : Polynomial R) => (Module.AEval.of R M a) (d ((Polynomial.aeval a) f)), map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

## Instances For

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`

.

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`

.