instPow — Mathlib

English

There is a power operation on MonoidHom M N: for f ∈ M →* N and n ∈ ℕ, the nth power f^n is the homomorphism defined by (f^n)(m) = f(m)^n.

Русский

Для отображений Морид-гомоморфизмов M →* N существует операция возведения в степень: если f ∈ M →* N и n ∈ ℕ, то f^n определяется как (f^n)(m) = f(m)^n.

LaTeX

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

Lean4

@[to_additive existing AddMonoidHom.instNatSMul]
instance instPow [MulOneClass M] [CommMonoid N] : Pow (M →* N) ℕ where
  pow f
    n :=
    { toFun := f ^ n
      map_one' := by simp
      map_mul' x y := by simp [mul_pow] }

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