English
There is a canonical equivalence between order-add-monoid isomorphisms and order-monoid isomorphisms of their multiplicative versions.
Русский
Существует каноническое эквивалентное соответствие между упорядоченными моноидными изоморфизмами и их умноженными версиями.
LaTeX
$$$ \mathrm{toMultiplicative}: \text{OrderAddMonoidIso}(G,H) \to \text{OrderMonoidIso}(\mathrm{Multiplicative}\,G, \mathrm{Multiplicative}\,H) $$$
Lean4
/-- Reinterpret `G ≃+o H` as `Multiplicative G ≃*o Multiplicative H`. -/
def toMultiplicative {G H : Type*} [AddCommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(G ≃+o H) ≃ (Multiplicative G ≃*o Multiplicative H)
where
toFun e := ⟨AddEquiv.toMultiplicative e, by simp⟩
invFun e := ⟨AddEquiv.toMultiplicative.symm e, by simp⟩
left_inv e := by ext; simp
right_inv e := by ext; simp
