English
For x ≠ y in a division ring K, and integers m ≤ n with x and y commuting, the sum over i ∈ Ico m n of x^i y^(n-1-i) equals (x^n − y^(n−m) x^m)/(x − y).
Русский
Для x ≠ y в делимом кольце K и при m ≤ n и commuting x,y сумма по 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,y]=0,\ x \neq y\;\Rightarrow\; \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 (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1) :=
by simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]
