English
Let M be a monoid and R a semiring. For any m ∈ M and r ∈ R, for every natural number n, the nth power of the basis element corresponding to m with coefficient r equals the basis element corresponding to m^n with coefficient r^n: (single m r)^n = single (m^n) (r^n).
Русский
Пусть M — моноид, R — полукольцо. Для любых m ∈ M и r ∈ R при любом натуральном n выполнено: (single m r)^n = single (m^n) (r^n).
LaTeX
$$$\\forall m \\in M, \\forall r \\in R, \\forall n \\in \\mathbb{N}, \\ (\\mathrm{single}\\, m\\, r)^n = \\mathrm{single}(m^n) (r^n).$$$
Lean4
@[to_additive (attr := simp) (dont_translate := R) single_pow]
theorem single_pow (m : M) (r : R) : ∀ n : ℕ, single m r ^ n = single (m ^ n) (r ^ n)
| 0 => by simp [one_def]
| n + 1 => by simp [pow_succ, single_pow _ _ n]
