eq_hilbertPoly_of_forall_coeff_eq_eval

English

For p ∈ F[X] and d ∈ ℕ, hilbertPoly(p * (1 - X)) (d + 1) = hilbertPoly(p) d.

Русский

Для любого p и d выполнено: hilbertPoly(p(1 - X), d+1) = hilbertPoly(p, d).

LaTeX

$$$\operatorname{hilbertPoly}(p \cdot (1 - X), d + 1) = \operatorname{hilbertPoly}(p, d)$$$

Lean4

/-- If `h : F[X]` and there exists some `N : ℕ` such that for any number `n : ℕ` bigger than `N`
we have `PowerSeries.coeff F n (p * invOneSubPow F d) = h.eval (n : F)`, then `h` is exactly
`Polynomial.hilbertPoly p d`.
-/
theorem eq_hilbertPoly_of_forall_coeff_eq_eval {p h : F[X]} {d : ℕ} (N : ℕ)
    (hhN : ∀ n > N, PowerSeries.coeff (R := F) n (p * invOneSubPow F d) = h.eval (n : F)) : h = hilbertPoly p d :=
  ExistsUnique.unique (existsUnique_hilbertPoly p d) ⟨N, hhN⟩
    ⟨p.natDegree, fun _ x => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d x⟩

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