English
If x and y commute, then the sum of x^i y^{n-1-i} over i equals the sum of y^i x^{n-1-i} over i (for all n).
Русский
Если x и y commuting, то сумма x^i y^{n-1-i} по i равна сумме y^i x^{n-1-i} (для всех n).
LaTeX
$$$\\forall n:\\, \\text{Commute}(x,y) \\Rightarrow \\sum_{i=0}^{n-1} x^{i} y^{n-1-i} = \\sum_{i=0}^{n-1} y^{i} x^{n-1-i}$$$
Lean4
protected theorem geom_sum₂_comm (n : ℕ) (h : Commute x y) :
∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i) :=
by
cases n; · simp
simp only [Nat.add_sub_cancel]
rw [← Finset.sum_flip]
refine Finset.sum_congr rfl fun i hi => ?_
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using
h.pow_pow _
_
-- TODO: for consistency, the next two lemmas should be moved to the root namespace
