Theorem Polynomial.leadingCoeff_preHilbertPoly

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