English
There is a natural equivalence (an isomorphism) between OrderMonoidIso G H and OrderMonoidIso (WithZero G) (WithZero H); this is a version of Equiv.optionCongr adapted to WithZero.
Русский
Существует естественное эквивалентное соответствие между OrderMonoidIso G H и OrderMonoidIso (WithZero G) (WithZero H); это версия Equiv.optionCongr, адаптированная к WithZero.
LaTeX
$$$(G \\simeq_*o H) \\simeq (WithZero G \\simeq_*o WithZero H)$$$
Lean4
/-- A version of `Equiv.optionCongr` for `WithZero` on `OrderMonoidIso`. -/
@[simps!]
def withZero {G H : Type*} [Group G] [PartialOrder G] [Group H] [PartialOrder H] :
(G ≃*o H) ≃ (WithZero G ≃*o WithZero H)
where
toFun e := ⟨e.toMulEquiv.withZero, fun {a b} ↦ by cases a <;> cases b <;> simp⟩
invFun e := ⟨MulEquiv.withZero.symm e, fun {a b} ↦ by simp⟩
left_inv _ := by ext; simp
right_inv _ := by ext x; cases x <;> simp
