English
For x in tsze.R M and any n, the second coordinate of x^n is the sum of n terms, each being a combination of powers of fst(x) and the snd-component x.snd, with the appropriate left and right actions of R on M.
Русский
Для x ∈ tsze.R M и любого n вторая координата x^n равна сумме из n слагаемых, каждая из которых является сочетанием степеней fst(x) и второй координаты x.snd с учётом соответствующих действий R на M.
LaTeX
$$$\\\\mathrm{snd}(x^n) = \\sum_{i=0}^{n-1} (\\\\operatorname{fst} x)^{\,n-1-i} \\\\cdot x.snd \\\\cdot (\\\\operatorname{fst} x)^i$$$
Lean4
theorem snd_pow_eq_sum [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (x : tsze R M)
(n : ℕ) : snd (x ^ n) = ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum :=
rfl
