English
If M and N are isomorphic as monoid objects, then for any X there is a canonical multiplicative equivalence between the hom-sets X → M and X → N, induced by the isomorphism e: M ≅ N.
Русский
Если M и N изоморфны как моноидальные объекты, существует каноническое умножательное эквивалентное отображение между множествами гомоморфизмов X → M и X → N, задаваемое изоморфизмом e: M ≅ N.
LaTeX
$$$ (\\!X \\to M\\!) \\; \\xrightarrow{\\simeq_\\text{Mul}}\\; (\\!X \\to N\\!) $$$
Lean4
/-- If `M` and `N` are isomorphic as monoid objects, then `X ⟶ M` and `X ⟶ N` are isomorphic
monoids. -/
@[simps!]
def mulEquivCongrRight (e : M ≅ N) [IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (X ⟶ N) :=
((yonedaMon.mapIso <| Mon.mkIso' e).app <| .op X).monCatIsoToMulEquiv
