geom_sum_succ — Mathlib

English

A standard relation for finite geometric sums: sum from i=0 to n-1 of (x)^i satisfies a recurrence with shift by one power.

Русский

Стандартная рекуррентность геометрической суммы для конечного ряда степеней x^i.

LaTeX

$$$\\sum_{i=0}^{n-1} x^{i} = x \\cdot \\sum_{i=0}^{n-2} x^{i} + 1$$$

Lean4

theorem geom_sum_succ {x : R} {n : ℕ} : ∑ i ∈ range (n + 1), x ^ i = (x * ∑ i ∈ range n, x ^ i) + 1 := by
  simp only [mul_sum, ← pow_succ', sum_range_succ', pow_zero]

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