Theorem Polynomial.preHilbertPoly_eq_choose_sub_add

Modification history

2026-08-26 20:09
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
refactor(RingTheory/Polynomial/HilbertPoly): generalize `preHilbertPoly_eq_choose_sub_add` (#43107) …
Deleted Polynomial.preHilbertPoly_eq_choose_sub_addView on Github →
2025-07-08 11:58
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
chore: whitespace fixes in lemmas (#26892) …
Modified Polynomial.preHilbertPoly_eq_choose_sub_addView on Github →
2024-12-02 18:04
Mathlib/RingTheory/Polynomial/HilbertPoly.lean
feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of `Polynomial.hilbertPoly p d` for `p : F[X]` and `d : ℕ`, where `F` is a field. (#19303) …
Added Polynomial.preHilbertPoly_eq_choose_sub_addView on Github →