PiLex

📁 Source: Mathlib/Algebra/Order/Group/PiLex.lean

Statistics

Metric	Count
Definitions	0
Theorems isOrderedAddCancelMonoid, isOrderedCancelMonoid	2
Total	2

Pi.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderedAddCancelMonoid 📖	mathematical	IsOrderedCancelAddMonoid PartialOrder.toPreorder	IsOrderedCancelAddMonoid Lex instAddCommMonoidLex Pi.addCommMonoid PartialOrder.toPreorder Pi.instPartialOrderLexForallOfLinearOrder	—	le_rfl add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLT covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid Eq.le add_left_cancel instIsLeftCancelAddLex Pi.instIsLeftCancelAdd IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd lt_of_add_lt_add_left
isOrderedCancelMonoid 📖	mathematical	IsOrderedCancelMonoid PartialOrder.toPreorder	IsOrderedCancelMonoid Lex instCommMonoidLex Pi.commMonoid PartialOrder.toPreorder Pi.instPartialOrderLexForallOfLinearOrder	—	le_rfl mul_lt_mul_left IsRightCancelMul.mulRightStrictMono_of_mulRightMono instIsRightCancelMulOfMulRightReflectLE contravariant_swap_mul_of_contravariant_mul IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instIsLeftCancelMulOfMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLE IsOrderedCancelMonoid.toMulLeftReflectLT covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid Eq.le mul_left_cancel instIsLeftCancelMulLex Pi.instIsLeftCancelMul IsCancelMul.toIsLeftCancelMul IsOrderedCancelMonoid.toIsCancelMul lt_of_mul_lt_mul_left'

---

← Back to Index