PiLex

Statistics

Metric	Count
Definitions	0
Theorems `isOrderedAddCancelMonoid`, `isOrderedCancelMonoid`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedAddCancelMonoid` 📖	mathematical	`IsOrderedCancelAddMonoid`	`Lex` `instAddCommMonoidLex` `Pi.addCommMonoid` `Pi.instPartialOrderLexForallOfLinearOrder`	—	`le_rfl` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `Eq.le` `add_left_cancel` `instIsLeftCancelAddLex` `Pi.instIsLeftCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `lt_of_add_lt_add_left` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isOrderedCancelMonoid` 📖	mathematical	`IsOrderedCancelMonoid`	`Lex` `instCommMonoidLex` `Pi.commMonoid` `Pi.instPartialOrderLexForallOfLinearOrder`	—	`le_rfl` `mul_lt_mul_left` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `IsCancelMul.toIsRightCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `Eq.le` `mul_left_cancel` `instIsLeftCancelMulLex` `Pi.instIsLeftCancelMul` `IsCancelMul.toIsLeftCancelMul` `lt_of_mul_lt_mul_left'` `IsOrderedCancelMonoid.toMulLeftReflectLT`

---