sum_of_finite — Mathlib

English

If p is a formal multilinear series with p_m = 0 for all m ≥ n, then for every x, p.sum x equals p.partialSum n x.

Русский

Если у формального многочленного ряда p все коэффициенты после степени n равны нулю, то для любого x выполняется p.sum x = p.partialSum n x.

LaTeX

$$$\\forall p:\\,\\text{FormalMultilinearSeries } 𝕜\\ E\\ F, \\forall n:\\mathbb{N}, (\\forall m:\\mathbb{N}, n \\le m \\Rightarrow p m = 0) \\Rightarrow \\forall x:\\, E,\\ p.sum\\ x = p.partialSum\\ n\\ x$$$

Lean4

protected theorem sum_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) (x : E) :
    p.sum x = p.partialSum n x :=
  tsum_eq_sum fun m hm ↦ by rw [Finset.mem_range, not_lt] at hm; rw [hn m hm]; rfl

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