Theorems · Definition · order theory

LinearOrder.mkOfGroupCone

{S : Type u_1} →
  {G : Type u_2} →
    [inst : CommGroup G] →
      [inst_1 : SetLike S G] →
        (C : S) → [GroupConeClass S G] → [HasMemOrInvMem C] → [DecidablePred fun x => x ∈ C] → LinearOrder G

Construct a linear order by designating a maximal cone in an abelian group.

Defined in

Mathlib.Algebra.Order.Group.Cone

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

CommGroupSetLikeGroupConeClassHasMemOrInvMemDecidablePred