Theorem Polynomial.hilbertPoly_mul_one_sub_succ

Modification history

2024-12-04 20:23

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

feat(RingTheory/Polynomial/Hilbert): `Polynomial.exists_unique_hilbertPoly` and `Polynomial.hilbertPoly_mul_one_sub_pow_add` (#19404)

Added Polynomial.hilbertPoly_mul_one_sub_succ View on Github →