instPow — Mathlib

English

There is a power operation on the endomorphism-type OneHom M N: for f ∈ OneHom M N and n ∈ ℕ, the nth power f^n is the endomorphism sending m to f(m)^n.

Русский

Существует операция возведения в степень для отображений, сопоставляющих единичному элементу, то есть для f ∈ OneHom M N и n ∈ ℕ выполняется f^n: M → N, определяемое как m ↦ f(m)^n.

LaTeX

$$$\forall f:\,M\to^1 N,\;\forall n\in\mathbb{N},\; (f^{n})(m)=f(m)^{n}.$$$

Lean4

@[to_additive existing ZeroHom.instNatSMul]
instance instPow [One M] [Monoid N] : Pow (OneHom M N) ℕ where
  pow f
    n :=
    { toFun := f ^ n
      map_one' := by simp }

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