geom_sum_of_lt_one — Mathlib

English

If x < 1 in a canonically ordered semifield, then ∑_{i=0}^{n-1} x^i = (1 − x^n)/(1 − x).

Русский

Если x < 1 в канонически упорядоченной полуполевой структуре, то сумма ∑_{i=0}^{n-1} x^i равна (1 − x^n)/(1 − x).

LaTeX

$$$\\sum_{i=0}^{n-1} x^i=\\frac{1-x^n}{1-x}$ при $x<1$$$

Lean4

theorem geom_sum_of_lt_one (h : x < 1) (n : ℕ) : ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x) :=
  eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_le_one h.le n)

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