toCommGrpIso — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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