Prod

📁 Source: Mathlib/Algebra/Order/Monoid/Prod.lean

Statistics

Metric	Count
Definitions	0
Theorems isOrderedAddCancelMonoid, isOrderedAddMonoid, isOrderedCancelMonoid, isOrderedMonoid, instCanonicallyOrderedAdd, instCanonicallyOrderedMul, instExistsAddOfLE, instExistsMulOfLE, instIsOrderedAddCancelMonoid, instIsOrderedAddMonoid, instIsOrderedCancelMonoid, instIsOrderedMonoid	12
Total	12

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd instAdd instLE_mathlib	—	instExistsAddOfLE CanonicallyOrderedAdd.toExistsAddOfLE le_def le_add_self le_self_add
instCanonicallyOrderedMul 📖	mathematical	—	CanonicallyOrderedMul instMul instLE_mathlib	—	instExistsMulOfLE CanonicallyOrderedMul.toExistsMulOfLE le_def le_mul_self le_self_mul
instExistsAddOfLE 📖	mathematical	—	ExistsAddOfLE instAdd instLE_mathlib	—	ExistsAddOfLE.exists_add_of_le
instExistsMulOfLE 📖	mathematical	—	ExistsMulOfLE instMul instLE_mathlib	—	ExistsMulOfLE.exists_mul_of_le
instIsOrderedAddCancelMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid instAddCommMonoid instPartialOrder	—	instIsOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid instAddCommMonoid instPartialOrder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
instIsOrderedCancelMonoid 📖	mathematical	—	IsOrderedCancelMonoid instCommMonoid instPartialOrder	—	instIsOrderedMonoid IsOrderedCancelMonoid.toIsOrderedMonoid le_of_mul_le_mul_left' IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT IsCancelMul.toIsLeftCancelMul IsOrderedCancelMonoid.toIsCancelMul IsOrderedCancelMonoid.toMulLeftReflectLT
instIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid instCommMonoid instPartialOrder	—	mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono

Prod.Lex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderedAddCancelMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid Lex instAddCommMonoidLex Prod.instAddCommMonoid instPartialOrder	—	isOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_iff lt_of_add_lt_add_left IsOrderedCancelAddMonoid.toAddLeftReflectLT add_left_cancel le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Lex instAddCommMonoidLex Prod.instAddCommMonoid instPartialOrder	—	le_iff add_lt_add_left covariant_swap_add_of_covariant_add add_le_add_left IsOrderedAddMonoid.toAddLeftMono
isOrderedCancelMonoid 📖	mathematical	—	IsOrderedCancelMonoid Lex instCommMonoidLex Prod.instCommMonoid instPartialOrder	—	isOrderedMonoid IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono IsCancelMul.toIsLeftCancelMul IsOrderedCancelMonoid.toIsCancelMul IsOrderedMonoid.toMulLeftMono IsOrderedCancelMonoid.toIsOrderedMonoid le_iff lt_of_mul_lt_mul_left' IsOrderedCancelMonoid.toMulLeftReflectLT mul_left_cancel le_of_mul_le_mul_left' IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT
isOrderedMonoid 📖	mathematical	—	IsOrderedMonoid Lex instCommMonoidLex Prod.instCommMonoid instPartialOrder	—	le_iff mul_lt_mul_left covariant_swap_mul_of_covariant_mul mul_le_mul_left IsOrderedMonoid.toMulLeftMono

---

← Back to Index