Order

📁 Source: Mathlib/Algebra/Ring/Subring/Order.lean

Statistics

Metric	Count
Definitions orderedSubtype	1
Theorems orderedSubtype_coe, toIsOrderedRing, toIsStrictOrderedRing	3
Total	4

Subring

Definitions

Name	Category	Theorems
orderedSubtype 📖	CompOp	1 math math: orderedSubtype_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderedSubtype_coe 📖	mathematical	—	RingHomClass.toRingHom OrderRingHom Subring SetLike.instMembership instSetLike Semiring.toNonAssocSemiring Ring.toSemiring toRing Subtype.preorder PartialOrder.toPreorder OrderRingHom.instFunLike OrderRingHom.instRingHomClass orderedSubtype subtype	—	OrderRingHom.instRingHomClass
toIsOrderedRing 📖	mathematical	—	IsOrderedRing SetLike.instMembership Ring.toSemiring SubringClass.toRing Subtype.partialOrder	—	Function.Injective.isOrderedRing
toIsStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing SetLike.instMembership Ring.toSemiring SubringClass.toRing Subtype.partialOrder	—	Function.Injective.isStrictOrderedRing

---

← Back to Index