derivative): change `polynomial.derivative` to be a `linear_map` (#5198)

Commit

5 years ago

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

Author

awainverse

Parents

240f6eb9

mathlib ad25cacf - refactor(data/polynomial/derivative): change `polynomial.derivative` to be a `linear_map` (#5198)

mathlib
ad25cacf - refactor(data/polynomial/derivative): change `polynomial.derivative` to be a `linear_map` (#5198)