mulEquivIsoGroupIso — Mathlib

English

Multiplicative equivalences between groups are equivalent to isomorphisms in GrpCat.

Русский

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

LaTeX

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

Lean4

/-- multiplicative equivalences between `Group`s are the same as (isomorphic to) isomorphisms
in `GrpCat` -/
@[to_additive]
def mulEquivIsoGroupIso {X Y : GrpCat.{u}} : X ≃* Y ≅ X ≅ Y
    where
  hom e := e.toGrpIso
  inv i := i.groupIsoToMulEquiv

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