Theorem Polynomial.eq_hilbertPoly_of_forall_coeff_eq_eval

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