English
There exists a unique h ∈ F[X] and N ∈ ℕ such that for all n > N, (p * invOneSubPow F d).coeff n = h.eval n, and h is hilbertPoly p d.
Русский
Существует единственный h ∈ F[X] и N ∈ ℕ such that для всех n > N равноcти вышеуказанному, и этот h = hilbertPoly p d.
LaTeX
$$$\exists! h : F[X], \exists N : \mathbb{N}, \forall n > N, (p * invOneSubPow F d).coeff\,n = h.eval (n) \\ \, \text{and } h = \operatorname{hilbertPoly}(p, d)$$$
Lean4
/-- The polynomial satisfying the key property of `Polynomial.hilbertPoly p d` is unique.
-/
theorem existsUnique_hilbertPoly (p : F[X]) (d : ℕ) :
∃! h : F[X], ∃ N : ℕ, ∀ n > N, (p * invOneSubPow F d : F⟦X⟧).coeff n = h.eval (n : F) :=
by
use hilbertPoly p d; constructor
· use p.natDegree
exact fun n => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d
· rintro h ⟨N, hhN⟩
apply eq_of_infinite_eval_eq h (hilbertPoly p d)
apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono
rintro x ⟨n, hn, rfl⟩
simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hn ⊢
rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]
