geom_sum_succ' — Mathlib

English

The geometric sum satisfies the identity sum_{i=0}^{n} x^{i} = x^{n} + sum_{i=0}^{n-1} x^{i}.

Русский

Геометрическая сумма удовлетворяет равенству: сумма от i=0 до n равна $x^{n} + \sum_{i=0}^{n-1} x^{i}$.

LaTeX

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

Lean4

theorem geom_sum_succ' {x : R} {n : ℕ} : ∑ i ∈ range (n + 1), x ^ i = x ^ n + ∑ i ∈ range n, x ^ i :=
  (sum_range_succ _ _).trans (add_comm _ _)

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