mulEquivIsoCommGroupIso — Mathlib

English

Multiplicative equivalences between commutative groups are equivalent to isomorphisms in CommGrpCat.

Русский

Умножаемые эквиваленты между коммутативными группами эквивалентны изоморфизмам в CommGrpCat.

LaTeX

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

Lean4

/-- Multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms
in `CommGrpCat`. -/
@[to_additive]
def mulEquivIsoCommGroupIso {X Y : CommGrpCat.{u}} : X ≃* Y ≅ X ≅ Y
    where
  hom e := e.toCommGrpIso
  inv i := i.commGroupIsoToMulEquiv

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