OrderDual

Statistics

Metric	Count
Definitions	0
Theorems `isOrderedAddCancelMonoid`, `isOrderedAddMonoid`, `isOrderedCancelMonoid`, `isOrderedMonoid`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedAddCancelMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `OrderDual` `instAddCommMonoid` `instPartialOrder`	—	`isOrderedAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `le_of_add_le_add_left` `addLeftReflectLE` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `OrderDual` `instAddCommMonoid` `instPartialOrder`	—	`add_le_add_left` `addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`isOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `OrderDual` `instCommMonoid` `instPartialOrder`	—	`isOrderedMonoid` `IsOrderedCancelMonoid.toIsOrderedMonoid` `le_of_mul_le_mul_left'` `mulLeftReflectLE` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT`
`isOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `OrderDual` `instCommMonoid` `instPartialOrder`	—	`mul_le_mul_left` `mulRightMono` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`

---