instIntPow — Mathlib

English

MonoidHom M N with N commutative supports integer powers: (f^k) for k ∈ ℤ satisfies the usual power rules.

Русский

MonoidHom M N с коммутативным N поддерживает целочисленные степени: (f^k) с k ∈ ℤ соблюдает обычные правила степеней.

LaTeX

$$$\text{MonoidHom } M N\text{ has }\mathbb{Z}\text{-power structure; }(f^k)(x)=f(x)^k.$$$

Lean4

@[to_additive existing AddMonoidHom.instIntSMul]
instance instIntPow [MulOneClass M] [CommGroup N] : Pow (M →* N) ℤ where
  pow f
    n :=
    { toFun := f ^ n
      map_one' := by simp
      map_mul' x y := by simp [mul_zpow] }

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