English
Let R be a commutative semiring with the usual order structure, and suppose y ≤ x. Then the product of the geometric sum ∑_{i=0}^{n-1} x^i y^{n-1-i} by (x − y) equals x^n − y^n.
Русский
Пусть R есть коммутативное полукольцо с упорядочиванием, и пусть y ≤ x. Тогда произведение геометрической суммы ∑_{i=0}^{n-1} x^i y^{n-1-i} на (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\\; (\\text{если } y \\le x).$$$
Lean4
theorem geom_sum₂_mul_of_ge (hxy : y ≤ x) (n : ℕ) :
(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n :=
by
apply eq_tsub_of_add_eq
simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n
