Commit 2026-08-26 20:09 3a806a8a
View on Github →refactor(RingTheory/Polynomial/HilbertPoly): generalize preHilbertPoly_eq_choose_sub_add (#43107)
This lemma also holds for the weaker hypothesis k ≤ n + d (where both sides evaluate to zero). Note that the statement needed to be changed slightly to avoid natural number subtraction giving zero.