Linearly ordered subgroups

Main definitions

• Subgroup.topOrderMonoidIso : the order preserving isomorphism from the top subgroup to the group.

noncomputable def Subgroup.topOrderMonoidIso (G : Type u_1) [Group G] [Preorder G] : ↥⊤ ≃*o G

The order preserving isomorphism from the top subgroup to the group.

Equations

• Subgroup.topOrderMonoidIso G = { toMulEquiv := Subgroup.topEquiv, map_le_map_iff' := ⋯ }