toNatPow — Mathlib

English

On any Monoid M, there is a natural-power operation defined by x^n = Monoid.npow n x.

Русский

На любом моноиде M существует естественная операция возведения в степень: x^n = Monoid.npow n x.

LaTeX

$$$\\forall M\\, [Monoid M],\\forall x\\in M,\\forall n\\in \\mathbb{N}: x^{n} = \\mathrm{npow}(n)\\,x$$$

Lean4

@[default_instance high]
instance toNatPow {M : Type*} [Monoid M] : Pow M ℕ :=
  ⟨fun x n ↦ Monoid.npow n x⟩

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