Commit 2024-09-11 12:15 ef71a8c9

View on Github →

feat(Algebra/Polynomial/Derivation): coefficient-wise derivation on a polynomial (#14702) Define Derivation.coeffwise, which applies the derivation to the a polynomial coefficient-wise.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Derivation/MapCoeffs.lean

added theorem Derivation.apply_aeval_eq'

added theorem Derivation.apply_aeval_eq

added theorem Derivation.apply_eval_eq

added def Derivation.mapCoeffs

added theorem Derivation.mapCoeffs_C

added theorem Derivation.mapCoeffs_X

added theorem Derivation.mapCoeffs_apply

added theorem Derivation.mapCoeffs_monomial