geom_sum_Ico' — Mathlib

English

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

Русский

Для x ≠ 1 и x ≠ 0 в делимом кольце K, и натурального n, сумма ∑ x^(−i) равна (x − 1)^(−1) (x − x^(−n) x).

LaTeX

$$$\forall x \in K, x \neq 1, x \neq 0, \forall n \in \mathbb{N}, \sum_{i=0}^{n-1} x^{-i} = (x-1)^{-1} (x - x^{-n} x)$$$

Lean4

theorem geom_sum_Ico' (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x) :=
  by simpa [geom_sum_Ico hx hmn] using neg_div_neg_eq (x ^ m - x ^ n) (1 - x)

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