geom_sum₂ — Mathlib

English

For any x ≠ 1 in a division ring K and natural n, the sum ∑_{i=0}^{n-1} x^i equals (x^n − 1)/(x − 1).

Русский

Для любого x ≠ 1 в деленном кольце K и целого n выполняется сумма геометрическая: ∑_{i=0}^{n-1} x^i = (x^n − 1)/(x − 1).

LaTeX

$$$\forall x \ne 1, \forall n \in \mathbb{N}, \sum_{i=0}^{n-1} x^i = \dfrac{x^n - 1}{x - 1}$$$

Lean4

protected theorem geom_sum₂ (h' : Commute x y) (h : x ≠ y) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y) :=
  by
  have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h'.geom_sum₂_mul, mul_div_cancel_right₀ _ this]

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