English
There is a canonical power operation on tsze_R M by natural numbers, defined via the formula for (r+m)^n.
Русский
Существует каноническое возведение в степень по естественным числам на tsze_R M, определяемое формулой для (r+m)^n.
LaTeX
$$$\text{Pow}(\mathrm{tsze}_{R} M, \mathbb{N})$ with \ (r+m)^n = r^n + \sum_{i=0}^{n-1} r^{(n-1-i)} m r^i$$$
Lean4
/-- In the general non-commutative case, the power operator is
$$\begin{align}
(r + m)^n &= r^n + r^{n-1}m + r^{n-2}mr + \cdots + rmr^{n-2} + mr^{n-1} \\
& =r^n + \sum_{i = 0}^{n - 1} r^{(n - 1) - i} m r^{i}
\end{align}$$
In the commutative case this becomes the simpler $(r + m)^n = r^n + nr^{n-1}m$.
-/
instance [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] : Pow (tsze R M) ℕ :=
⟨fun x n => ⟨x.fst ^ n, ((List.range n).map fun i => x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i).sum⟩⟩
