English
The induced left-right order equivalences mirror cone membership with H-divisibility in a group.
Русский
Пороговая связка между порядком и членством в конусе и делимостью в группе.
LaTeX
$$$\forall S,G\ [CommGroup G] [SetLike S G]\ [GroupConeClass S G]\ {C:S}\ {a,b:G},\ le_{(mkOfGroupCone C)}\ a b \iff b\/a \in C$$
Lean4
/-- Construct a partially ordered abelian group by designating a cone in an abelian group. -/
@[to_additive /-- Construct a partially ordered abelian group by designating a cone in an abelian group. -/
]
theorem mkOfCone [GroupConeClass S G] :
let _ : PartialOrder G := PartialOrder.mkOfGroupCone C
IsOrderedMonoid G :=
let _ : PartialOrder G := PartialOrder.mkOfGroupCone C
{ mul_le_mul_left := fun a b nab c ↦ by simpa [· ≤ ·] using nab }
