Theorem Polynomial.coeff_preHilbertPoly_self

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