Theorems · Inductive type · order theory
GroupCone
(G : Type u_1) → [CommGroup G] → Type u_1
A (positive) cone in an abelian group is a submonoid that
does not contain both a and a⁻¹ for any non-identity a.
This is equivalent to being the set of elements that are at least 1 in
some order making the group into a partially ordered group.
- Defined in
- Mathlib.Algebra.Order.Group.Cone
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommGroupstatement · cited by 990
Cited by15
Results whose statement or proof uses this declaration.
- GroupCone.oneLEstatement · cited by 4
- GroupCone.toSubmonoidstatement and proof · cited by 2
- GroupCone.mk.injstatement · cited by 1
- GroupCone.mk.noConfusionstatement · cited by 1
- GroupCone.noConfusionTypestatement and proof · cited by 0
- GroupCone.recOnstatement and proof · cited by 0
- GroupCone.mk.injEqstatement · cited by 0
- GroupCone.mk.sizeOf_specstatement · cited by 0
- GroupCone.oneLE.congr_simpstatement · cited by 0
- GroupCone.casesOnstatement and proof · cited by 0
- GroupCone.coe_oneLEstatement · cited by 0
- GroupCone.ctorIdxstatement and proof · cited by 0