pow — Mathlib

English

Exponentiation from natural numbers to powers: for any base n in a monoid M and any natural m, there is a canonical element of the submonoid powers(n) corresponding to n^m.

Русский

Порождено натуральных степеней: для основы n в моноиде M и любого натурального m существует соответствующий элемент n^m внутри подмоноида powers(n).

LaTeX

$$$ \\text{pow}(n,m) = \\text{element in } \\operatorname{powers}(n) \\text{ corresponding to } n^m $$$

Lean4

/-- Exponentiation map from natural numbers to powers. -/
@[simps!]
def pow (n : M) (m : ℕ) : powers n :=
  (powersHom M n).mrangeRestrict (Multiplicative.ofAdd m)

Похожие утверждения