geom_sum_eq — Mathlib

English

For x ≠ 1 in a division ring K, and integers m ≤ n, the sum over i in Ico m n of x^i equals (x^n − x^m)/(x − 1).

Русский

Для x ≠ 1 в делимом кольце K и любых m ≤ n сумма по i ∈ Ico m n от x^i равна (x^n − x^m)/(x − 1).

LaTeX

$$$\forall x \ne 1, \forall m,n \ (m \le n), \sum_{i \in \mathrm{Ico}(m,n)} x^i = \dfrac{x^n - x^m}{x - 1}$$$

Lean4

theorem geom_sum_eq (h : x ≠ 1) (n : ℕ) : ∑ i ∈ range n, x ^ i = (x ^ n - 1) / (x - 1) :=
  by
  have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← geom_sum_mul, mul_div_cancel_right₀ _ this]

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