Order

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

Statistics

Metric	Count
Definitions nonneg	1
Theorems coe_nonneg, mem_nonneg, nonneg_toAddSubmonoid, toIsOrderedRing, toIsStrictOrderedRing, toIsOrderedRing, toIsStrictOrderedRing	7
Total	8

Subsemiring

Definitions

Name	Category	Theorems
nonneg 📖	CompOp	4 math math: RingCone.nonneg_toSubsemiring, nonneg_toAddSubmonoid, mem_nonneg, coe_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_nonneg 📖	mathematical	—	SetLike.coe Subsemiring Semiring.toNonAssocSemiring instSetLike nonneg AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.toAddSubsemigroup AddSubmonoid.nonneg PartialOrder.toPreorder	—	—
mem_nonneg 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike nonneg Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
nonneg_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid Semiring.toNonAssocSemiring nonneg AddSubmonoid.nonneg AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne PartialOrder.toPreorder IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsOrderedRing.toIsOrderedAddMonoid	—	—
toIsOrderedRing 📖	mathematical	—	IsOrderedRing Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toSemiring Subtype.partialOrder	—	SubsemiringClass.toIsOrderedRing instSubsemiringClass
toIsStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike toSemiring Subtype.partialOrder	—	SubsemiringClass.toIsStrictOrderedRing instSubsemiringClass

SubsemiringClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedRing 📖	mathematical	—	IsOrderedRing SetLike.instMembership toSemiring Subtype.partialOrder	—	Function.Injective.isOrderedRing
toIsStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing SetLike.instMembership toSemiring Subtype.partialOrder	—	Function.Injective.isStrictOrderedRing

---

← Back to Index