Two-variable geometric sums in a noncommutative semiring

Mathlib's Commute.geom_sum₂_mul_add and its relatives evaluate the two-variable geometric sum S = ∑_{i < m} x ^ i * y ^ (m - 1 - i) when x and y commute. Without that hypothesis S still satisfies a telescoping identity, x * S + y ^ m = S * y + x ^ m. In a ring it says that S intertwines x and y up to the error x ^ m - y ^ m, so S is an exact intertwiner x * S = S * y as soon as x ^ m = y ^ m.

Main result

• TauCeti.mul_geom_sum₂_add_pow: x * S + y ^ m = S * y + x ^ m in any semiring.

theorem TauCeti.mul_geom_sum₂_add_pow {S : Type u_1} [Semiring S] (x y : S) (m : ℕ) : x * ∑ i ∈ Finset.range m, x ^ i * y ^ (m - 1 - i) + y ^ m = (∑ i ∈ Finset.range m, x ^ i * y ^ (m - 1 - i)) * y + x ^ m

Telescoping a two-variable geometric sum in a noncommutative semiring: x * S + y ^ m = S * y + x ^ m for S = ∑_{i < m} x ^ i * y ^ (m - 1 - i).