Theorem Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one

Modification history

2024-12-09 08:03

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

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

Added Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one View on Github →