mulEquivIsoCommMonCatIso — Mathlib

English

There is an equivalence between MulEquiv X Y and Iso (CommMonCat.of X) (CommMonCat.of Y); multiplicative equivalences between commutative monoids correspond to isomorphisms in CommMonCat.

Русский

Существет эквивалентность между MulEquiv X Y и Iso (CommMonCat.of X) (CommMonCat.of Y).

LaTeX

$$$X \simeq_* Y \cong\; CommMonCat.of X \cong CommMonCat.of Y.$$$

Lean4

/-- multiplicative equivalences between `CommMonoid`s are the same as (isomorphic to) isomorphisms
in `CommMonCat` -/
@[to_additive addEquivIsoAddCommMonCatIso]
def mulEquivIsoCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] : X ≃* Y ≅ CommMonCat.of X ≅ CommMonCat.of Y
    where
  hom e := e.toCommMonCatIso
  inv i := i.commMonCatIsoToMulEquiv

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