English
There is an equivalence between MulEquiv X Y and Iso (MonCat.of X) (MonCat.of Y); i.e., multiplicative equivalences between monoids correspond to isomorphisms in MonCat.
Русский
Существует эквивалентность между MulEquiv X Y и Iso(MonCat.of X) (MonCat.of Y); то есть эквивалентности умножения между моноидами соответствуют изоморфизмы в MonCat.
LaTeX
$$$X \simeq_* Y \cong\; MonCat.of X \cong MonCat.of Y.$$$
Lean4
/-- multiplicative equivalences between `Monoid`s are the same as (isomorphic to) isomorphisms
in `MonCat` -/
@[to_additive addEquivIsoAddMonCatIso]
def mulEquivIsoMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] : X ≃* Y ≅ MonCat.of X ≅ MonCat.of Y
where
hom e := e.toMonCatIso
inv i := i.monCatIsoToMulEquiv
