instGroup — Mathlib

English

MonoidHom M N inherits integer powers when N is a group; the map (f^n) is defined for n ∈ ℤ.

Русский

MonoidHom M N наследует целочисленные степени, когда N является группой; определено f^n для n ∈ ℤ.

LaTeX

$$$\text{MonoidHom } M N\text{ with IntPow over }\mathbb{Z}$$$

Lean4

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

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