geom_sum₂_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem geom_sum₂_Ico (h : Commute x y) (hxy : x ≠ y) {m n : ℕ} (hmn : m ≤ n) :
    ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y) :=
  by
  have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

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