Commit 2024-12-09 08:03 bd9aea4b

View on Github →

feat(RingTheory/Polynomial/HilbertPoly): Polynomial.natDegree_hilbertPoly_of_ne_zero (#19765)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/Domain.lean

added theorem Polynomial.natDegree_smul

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

added theorem Polynomial.coeff_preHilbertPoly_self

added theorem Polynomial.eq_hilbertPoly_of_forall_coeff_eq_eval

added theorem Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one

added theorem Polynomial.leadingCoeff_preHilbertPoly

added theorem Polynomial.natDegree_hilbertPoly_of_ne_zero

added theorem Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt

added theorem Polynomial.natDegree_preHilbertPoly