instCommGroup — Mathlib

English

MonoidHom M N has a Pow by Int for group N; (f^n) defined for n ∈ ℤ with (f^0)=1 and (f^{n+1})=f^n f.

Русский

MonoidHom имеет степень по целым числам; (f^n) определено для n ∈ ℤ, с (f^0)=1 и (f^{n+1})=f^n f.

LaTeX

$$$\forall f:\,M\to^*N,\forall n:\mathbb{Z},\; (f^{n})(x)=f(x)^{n}$$$

Lean4

/-- If `G` is a commutative group, then so is `OneHom M G`. -/
@[to_additive /-- If `G` is an additive commutative group, then so is `ZeroHom M G`. -/
    ]
instance instCommGroup [One M] [CommGroup N] : CommGroup (OneHom M N) :=
  fast_instance%DFunLike.coe_injective.commGroup DFunLike.coe rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
      (fun _ _ => rfl) (fun _ _ => rfl)

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