English
There is a natural power operation on submodules of an algebra, defined by taking the n-fold product of a submodule with itself inside the ambient algebra. Concretely, for any submodule M and natural number n, the n-th power M^n is defined by repeated multiplication of M with itself, i.e., M^n is the n-fold product of M.
Русский
Существует естественная операция возведения подмодуля в степень над алгеброй: M^n есть n-кратное произведение подмодуля M с самим собой внутри окружной алгебры. Конкретно для подмодуля M и натурального числа n степень n задаётся как n-кратное произведение M самой с собой.
LaTeX
$$$M^n = \underbrace{M \cdot M \cdots M}_{n \text{ факторов}}$$$
Lean4
instance : Pow (Submodule R A) ℕ where pow s n := npowRec n s
