Commit 2023-08-02 18:06 30202c4a

View on Github →

feat: derivations of (univariate) polynomials (#6023) An R-derivation from R[X] is determined by its value on X. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed MvPolynomial.Derivation .

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/MvPolynomial/Derivation.lean

deleted theorem MvPolynomial.derivation_C_mul'

Modified Mathlib/Data/MvPolynomial/PDeriv.lean

modified theorem MvPolynomial.pderiv_C_mul

Created Mathlib/Data/Polynomial/Derivation.lean

added theorem Polynomial.C_smul_derivation_apply

added theorem Polynomial.derivation_C

added theorem Polynomial.derivation_ext

added def Polynomial.derivative'

added def Polynomial.mkDerivation

added def Polynomial.mkDerivationEquiv

added theorem Polynomial.mkDerivationEquiv_apply

added theorem Polynomial.mkDerivationEquiv_symm_apply

added theorem Polynomial.mkDerivation_X

added theorem Polynomial.mkDerivation_apply

added theorem Polynomial.mkDerivation_one_eq_derivative'

added theorem Polynomial.mkDerivation_one_eq_derivative