English
Let R be a commutative semiring. For any elements x, y in R and any natural number n, the two geometric-type sums ∑_{i=0}^{n-1} x^i y^{n-1-i} and ∑_{i=0}^{n-1} y^i x^{n-1-i} are equal.
Русский
Пусть R — коммутативная полукольцевая структура. Для любых элементов x, y ∈ R и натурального числа n равны двумерные геометрические суммы: сумма по i от 0 до n−1 of x^i y^{n−1−i} и сумма по i от 0 до n−1 of y^i x^{n−1−i}. Эти суммы равны между собой.
LaTeX
$$$\\displaystyle \\sum_{i=0}^{n-1} x^i y^{n-1-i} = \\sum_{i=0}^{n-1} y^i x^{n-1-i}$$$
Lean4
theorem geom_sum₂_comm (x y : R) (n : ℕ) :
∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i) :=
(Commute.all x y).geom_sum₂_comm n
