toGrpIso — Mathlib

English

From a MulEquiv between groups, one obtains a group isomorphism in GrpCat.

Русский

Из MulEquiv между группами получается изоморфизм групп в GrpCat.

LaTeX

$$$$ \forall X,Y:\mathrm{GrpCat},\; (e: X \simeq_* Y) \Rightarrow X \cong Y. $$$$

Lean4

/-- Build an isomorphism in the category `GrpCat` from a `MulEquiv` between `Group`s. -/
@[to_additive (attr := simps)]
def toGrpIso {X Y : GrpCat} (e : X ≃* Y) : X ≅ Y
    where
  hom := GrpCat.ofHom e.toMonoidHom
  inv := GrpCat.ofHom e.symm.toMonoidHom

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