Theorem Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt

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.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt View on Github →