Theorems · Inductive type · order theory
GroupConeClass
(S : Type u_1) → (G : outParam (Type u_2)) → [CommGroup G] → [SetLike S G] → Prop
GroupConeClass S G says that S is a type of cones in G.
- Defined in
- Mathlib.Algebra.Order.Group.Cone
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by7
Results whose statement or proof uses this declaration.
- PartialOrder.mkOfGroupConestatement and proof · cited by 2
- IsOrderedMonoid.mkOfConestatement and proof · cited by 0
- PartialOrder.mkOfGroupCone_le_iffstatement and proof · cited by 0
- GroupConeClass.casesOnstatement and proof · cited by 0
- GroupConeClass.eq_one_of_mem_of_inv_memstatement and proof · cited by 0
- GroupConeClass.recOnstatement and proof · cited by 0
- LinearOrder.mkOfGroupConestatement and proof · cited by 0