instIntPow — Mathlib

English

If M has One and N is a Group, then OneHom M N carries a Pow by Int, i.e., f^k for k ∈ ℤ.

Русский

Если M имеет единицу, а N — группу, то OneHom M N поддерживает возведение в степень целого типа: f^k для k ∈ ℤ.

LaTeX

$$$\text{OneHom } M N\text{ has a } \mathbb{Z}\text{-power structure for }[One M],[Group N].$$$

Lean4

@[to_additive existing ZeroHom.instIntSMul]
instance instIntPow [One M] [Group N] : Pow (OneHom M N) ℤ where
  pow f
    n :=
    { toFun := f ^ n
      map_one' := by simp }

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