English
For any ring R and commuting elements x, y, the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1-i} satisfies the same product identity as in the commutative case: (sum) (x − y) = x^n − y^n.
Русский
Для кольца R и коммутируемых элементов x, y справедлива та же формула геометрической суммы: (сумма) (x − y) = x^n − y^n.
LaTeX
$$$\\displaystyle \\left(\\sum_{i=0}^{n-1} x^i y^{n-1-i}\\right) (x - y) = x^n - y^n$$$
Lean4
protected theorem geom_sum₂_mul (h : Commute x y) (n : ℕ) :
(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n :=
by
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
rw [sub_add_cancel] at this
rw [← this, add_sub_cancel_right]
