Ring

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

Statistics

Metric	Count
Definitions linearOrderedCommMonoidWithZero	1
Theorems canonicallyOrderedAdd, existsAddOfLE, instNontrivialSubtypeLeOfNatOfAddLeftMono, isOrderedAddMonoid, isOrderedCancelAddMonoid, isOrderedRing, isStrictOrderedRing, noZeroDivisors, nontrivial, orderedSub	10
Total	11

Nonneg

Definitions

Name	Category	Theorems
linearOrderedCommMonoidWithZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing add AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid Ring.toSemiring	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid sub_nonneg_of_le covariant_swap_add_of_covariant_add add_sub_cancel le_add_of_nonneg_left isOrderedAddMonoid le_add_of_nonneg_right
existsAddOfLE 📖	mathematical	—	ExistsAddOfLE Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring add AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing ExistsAddOfLE.exists_add_of_le Subtype.coe_le_coe le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toAddLeftReflectLT add_zero
instNontrivialSubtypeLeOfNatOfAddLeftMono 📖	mathematical	—	Nontrivial Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	exists_ne Ne.lt_or_gt neg_nonneg LT.lt.le Subtype.coe_ne_coe neg_ne_zero
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid IsOrderedAddMonoid.toAddLeftMono Subtype.partialOrder	—	Function.Injective.isOrderedAddMonoid IsOrderedAddMonoid.toAddLeftMono coe_add
isOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid Subtype.partialOrder	—	Function.Injective.isOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid coe_add
isOrderedRing 📖	mathematical	—	IsOrderedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring IsOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Subtype.partialOrder	—	Function.Injective.isOrderedRing IsOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono coe_zero coe_one coe_add coe_mul
isStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Subtype.partialOrder	—	Function.Injective.isStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono coe_zero coe_one coe_add coe_mul
noZeroDivisors 📖	mathematical	—	NoZeroDivisors Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul IsOrderedRing.toPosMulMono zero	—	IsOrderedRing.toPosMulMono mul_nonneg
nontrivial 📖	mathematical	—	Nontrivial Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	IsStrictOrderedRing.toZeroLEOneClass zero_ne_one NeZero.charZero_one IsStrictOrderedRing.toCharZero
orderedSub 📖	mathematical	—	OrderedSub Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing add AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid Ring.toSemiring IsStrictOrderedRing.toIsOrderedRing sub Lattice.toSemilatticeSup SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add add_nonneg

---

← Back to Index