English
Under the same commuting actions, the snd-coordinate of x^n can also be written as snd(x^n) = n • (x.snd <• fst(x)^{n-1}), i.e., the left action by fst(x)^{n-1} is used before applying x.snd.
Русский
При тех же коммутативных действиях snd(x^n) может быть записано как snd(x^n) = n • (x.snd <• fst(x)^{n-1}), то есть сначала действует левая координата fst(x)^{n-1}, затем x.snd.
LaTeX
$$$\\\\mathrm{snd}(x^n) = n \\\\cdot (x.snd \\leftarrow (\\\\operatorname fst(x))^{n-1})$$$
Lean4
theorem snd_pow_of_smul_comm' [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ) (h : x.snd <• x.fst = x.fst •> x.snd) :
snd (x ^ n) = n • (x.snd <• x.fst ^ n.pred) := by rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]
