Mathlib Map

Theorems · Inductive type · order theory

RingConeClass

(S : Type u_1) → (R : outParam (Type u_2)) → [Ring R] → [SetLike S R] → Prop

RingConeClass S R says that S is a type of cones in R.

Defined in
Mathlib.Algebra.Order.Ring.Cone
Cited by
2 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
RingSetLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

RingConeClass.casesOn · cited by 0RingConeClass.casesOnRingConeClass.recOn · cited by 0RingConeClass.recOnRingConeClass.toSubmonoidClass · cited by 0RingConeClass.toSubmonoid…IsOrderedRing.mkOfCone · cited by 0IsOrderedRing.mkOfConeRing · cited by 7463RingSetLike · cited by 1084SetLikeRingConeClassCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Ringstatement · cited by 7,463
  • SetLikestatement · cited by 1,084

Cited by4

Results whose statement or proof uses this declaration.