Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 17:50 56a59d3e

View on Github →

feat(data/polynomial/hasse_deriv): Hasse derivatives (#8998)

Estimated changes

Modified src/data/polynomial/coeff.lean

added def polynomial.lsum

Created src/data/polynomial/hasse_deriv.lean

added theorem polynomial.factorial_smul_hasse_deriv

added def polynomial.hasse_deriv

added theorem polynomial.hasse_deriv_C

added theorem polynomial.hasse_deriv_X

added theorem polynomial.hasse_deriv_apply

added theorem polynomial.hasse_deriv_apply_one

added theorem polynomial.hasse_deriv_coeff

added theorem polynomial.hasse_deriv_comp

added theorem polynomial.hasse_deriv_monomial

added theorem polynomial.hasse_deriv_mul

added theorem polynomial.hasse_deriv_one'

added theorem polynomial.hasse_deriv_one

added theorem polynomial.hasse_deriv_zero'

added theorem polynomial.hasse_deriv_zero