hilbertPoly_mul_one_sub_succ — Mathlib

English

If h satisfies the large-n coefficient-evaluation property, then h = hilbertPoly p d.

Русский

Если h удовлетворяет условию на коэффициенты для больших n, то h = hilbertPoly p d.

LaTeX

$$$\exists N, (\forall n > N, (p * invOneSubPow F d).coeff n = h.eval (n)) \Rightarrow h = \operatorname{hilbertPoly}(p, d)$$$

Lean4

theorem hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) : hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d :=
  by
  apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree
  intro n hn
  have heq : 1 - PowerSeries.X = ((1 - X : F[X]) : F⟦X⟧) := by simp only [coe_sub, coe_one, coe_X]
  rw [← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one, ← mul_assoc, heq, ← coe_mul,
    coeff_mul_invOneSubPow_eq_hilbertPoly_eval (d + 1) hn]

Похожие утверждения