InjSurj

Statistics

Metric	Count
Definitions	0
Theorems `isOrderedRing`, `isStrictOrderedRing`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedRing` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Preorder.toLE` `PartialOrder.toPreorder`	`IsOrderedRing`	—	`isOrderedAddMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono`
`isStrictOrderedRing` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`IsStrictOrderedRing`	—	`isOrderedCancelAddMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `domain_nontrivial` `IsStrictOrderedRing.toNontrivial` `isOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono`

---