geom_sum₂_Ico — Mathlib

English

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

Русский

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

LaTeX

$$$\forall x,y\in K,\ x \neq y \Rightarrow \forall m,n\ (m \le n),\; \sum_{i \in \mathrm{Ico}(m,n)} x^i y^{n-1-i} = \dfrac{x^n - y^{n-m} x^m}{x - y}$$$

Lean4

theorem geom_sum₂_Ico (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) :=
  (Commute.all x y).geom_sum₂_Ico hxy hmn

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