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