Commit 2023-03-13 11:56 ac9d2970

View on Github →

feat: Port Data.Polynomial.HasseDeriv (#2842)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/HasseDeriv.lean

added theorem Polynomial.factorial_smul_hasseDeriv

added def Polynomial.hasseDeriv

added theorem Polynomial.hasseDeriv_C

added theorem Polynomial.hasseDeriv_X

added theorem Polynomial.hasseDeriv_apply

added theorem Polynomial.hasseDeriv_apply_one

added theorem Polynomial.hasseDeriv_coeff

added theorem Polynomial.hasseDeriv_comp

added theorem Polynomial.hasseDeriv_eq_zero_of_lt_natDegree

added theorem Polynomial.hasseDeriv_monomial

added theorem Polynomial.hasseDeriv_mul

added theorem Polynomial.hasseDeriv_one'

added theorem Polynomial.hasseDeriv_one

added theorem Polynomial.hasseDeriv_zero'

added theorem Polynomial.hasseDeriv_zero

added theorem Polynomial.natDegree_hasseDeriv

added theorem Polynomial.natDegree_hasseDeriv_le