ofHom — Mathlib

English

The morphism in FiniteGrp induced from a group hom f: X → Y is given by FiniteGrp.ofHom f.

Русский

Гомоморфизм в FiniteGrp, полученный из гомоморфизма группы f: X → Y, задается через FiniteGrp.ofHom f.

LaTeX

$$$$ \mathrm{FiniteGrp.ofHom}(f) : \mathrm{FiniteGrp.of}(X) \to \mathrm{FiniteGrp.of}(Y) $$$$

Lean4

/-- The morphism in `FiniteGrp`, induced from a morphism of the category `GrpCat`. -/
@[to_additive /-- The morphism in `FiniteAddGrp`, induced from a morphism of the category `AddGrpCat` -/
    ]
def ofHom {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) : of X ⟶ of Y :=
  GrpCat.ofHom f

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