Theorem Polynomial.preHilbertPoly_eq_choose_add_sub

Modification history

2026-08-26 20:09
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
refactor(RingTheory/Polynomial/HilbertPoly): generalize `preHilbertPoly_eq_choose_sub_add` (#43107) …
Added Polynomial.preHilbertPoly_eq_choose_add_subView on Github →