Commit 2020-12-04 07:42 ad25cacf

View on Github →

refactor(data/polynomial/derivative): change polynomial.derivative to be a linear_map (#5198) Refactors polynomial.derivative to be a linear_map by default

Estimated changes

Modified src/data/polynomial/derivative.lean

modified def polynomial.derivative

added theorem polynomial.derivative_apply

added theorem polynomial.derivative_eval

deleted def polynomial.derivative_hom

deleted def polynomial.derivative_lhom

modified theorem polynomial.derivative_zero

Modified src/data/polynomial/identities.lean

deleted theorem polynomial.derivative_eval