Commit 2023-06-13 06:31 765d9107

View on Github →

feat: port RingTheory.Polynomial.Hermite.Basic (#3967)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

added theorem Polynomial.coeff_hermite

added theorem Polynomial.coeff_hermite_explicit

added theorem Polynomial.coeff_hermite_of_even_add

added theorem Polynomial.coeff_hermite_of_lt

added theorem Polynomial.coeff_hermite_of_odd_add

added theorem Polynomial.coeff_hermite_self

added theorem Polynomial.coeff_hermite_succ_succ

added theorem Polynomial.coeff_hermite_succ_zero

added theorem Polynomial.degree_hermite

added theorem Polynomial.hermite_eq_iterate

added theorem Polynomial.hermite_monic

added theorem Polynomial.hermite_one

added theorem Polynomial.hermite_succ

added theorem Polynomial.hermite_zero

added theorem Polynomial.leadingCoeff_hermite

added theorem Polynomial.natDegree_hermite