geom_sum_of_one_lt — Mathlib

English

If x > 1 in a canonically ordered semifield, then the finite geometric sum equals (x^n − 1)/(x − 1).

Русский

Если x > 1 в канонически упорядоченной полуполевой системе, то сумма геометрического ряда длины n равна (x^n − 1)/(x − 1).

LaTeX

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

Lean4

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

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