English
For commuting x, y, the sum over range n+1 satisfies a relation: the total equals x^n + y times the sum over range n of x^i y^{n-1-i}.
Русский
Для коммутируемых x, y сумма по диапазону n+1 равна x^n плюс y на сумму по диапазону n от x^i y^{n-1-i}.
LaTeX
$$$\\displaystyle \\sum_{i=0}^{n} x^i y^{n-i} = x^n + y \\left(\\sum_{i=0}^{n-1} x^i y^{n-1-i}\\right)$$$
Lean4
protected theorem geom_sum₂_succ_eq (h : Commute x y) {n : ℕ} :
∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) :=
by
simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
(h.symm.pow_right _).eq, mul_assoc, ← pow_succ']
refine sum_congr rfl fun i hi => ?_
suffices n - 1 - i + 1 = n - i by rw [this]
rw [Finset.mem_range] at hi
cutsat
