Pi

📁 Source: Mathlib/Algebra/Order/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems const_le_one, const_le_one_of_le_one, const_lt_one, const_neg', const_nonneg, const_nonneg_of_nonneg, const_nonpos, const_nonpos_of_nonpos, const_pos, extend_le_one, extend_nonneg, extend_nonpos, one_le_const, one_le_const_of_one_le, one_le_extend, one_lt_const, existsAddOfLe, existsMulOfLe, instCanonicallyOrderedAddForall, instCanonicallyOrderedMulForall, isOrderedAddCancelMonoid, isOrderedAddMonoid, isOrderedCancelMonoid, isOrderedMonoid, isOrderedRing, mulSingle_le_mulSingle, mulSingle_le_one, one_le_mulSingle, one_lt_mulSingle, single_le_single, single_nonneg, single_nonpos, single_pos	33
Total	33

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_le_one 📖	mathematical	—	Pi.hasLe Preorder.toLE Pi.instOne	—	const_le_const
const_le_one_of_le_one 📖	mathematical	Preorder.toLE	Pi.hasLe Preorder.toLE Pi.instOne	—	—
const_lt_one 📖	mathematical	—	Preorder.toLT Pi.preorder Pi.instOne	—	const_lt_const
const_neg' 📖	mathematical	—	Preorder.toLT Pi.preorder Pi.instZero	—	const_lt_const
const_nonneg 📖	mathematical	—	Pi.hasLe Preorder.toLE Pi.instZero	—	const_le_const
const_nonneg_of_nonneg 📖	mathematical	Preorder.toLE	Pi.hasLe Preorder.toLE Pi.instZero	—	—
const_nonpos 📖	mathematical	—	Pi.hasLe Preorder.toLE Pi.instZero	—	const_le_const
const_nonpos_of_nonpos 📖	mathematical	Preorder.toLE	Pi.hasLe Preorder.toLE Pi.instZero	—	—
const_pos 📖	mathematical	—	Preorder.toLT Pi.preorder Pi.instZero	—	const_lt_const
extend_le_one 📖	mathematical	Pi.hasLe Pi.instOne	Pi.hasLe extend Pi.instOne	—	dite_le_one
extend_nonneg 📖	mathematical	Pi.hasLe Pi.instZero	Pi.hasLe Pi.instZero extend	—	dite_nonneg
extend_nonpos 📖	mathematical	Pi.hasLe Pi.instZero	Pi.hasLe extend Pi.instZero	—	dite_nonpos
one_le_const 📖	mathematical	—	Pi.hasLe Preorder.toLE Pi.instOne	—	const_le_const
one_le_const_of_one_le 📖	mathematical	Preorder.toLE	Pi.hasLe Preorder.toLE Pi.instOne	—	—
one_le_extend 📖	mathematical	Pi.hasLe Pi.instOne	Pi.hasLe Pi.instOne extend	—	one_le_dite
one_lt_const 📖	mathematical	—	Preorder.toLT Pi.preorder Pi.instOne	—	const_lt_const

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsAddOfLe 📖	mathematical	ExistsAddOfLE	ExistsAddOfLE instAdd hasLe	—	ExistsAddOfLE.exists_add_of_le
existsMulOfLe 📖	mathematical	ExistsMulOfLE	ExistsMulOfLE instMul hasLe	—	ExistsMulOfLE.exists_mul_of_le
instCanonicallyOrderedAddForall 📖	mathematical	CanonicallyOrderedAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Preorder.toLE PartialOrder.toPreorder	CanonicallyOrderedAdd instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass hasLe Preorder.toLE PartialOrder.toPreorder	—	existsAddOfLe CanonicallyOrderedAdd.toExistsAddOfLE le_add_self le_self_add
instCanonicallyOrderedMulForall 📖	mathematical	CanonicallyOrderedMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Preorder.toLE PartialOrder.toPreorder	CanonicallyOrderedMul instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass hasLe Preorder.toLE PartialOrder.toPreorder	—	existsMulOfLe CanonicallyOrderedMul.toExistsMulOfLE le_mul_self le_self_mul
isOrderedAddCancelMonoid 📖	mathematical	IsOrderedCancelAddMonoid	IsOrderedCancelAddMonoid addCommMonoid preorder	—	isOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsOrderedCancelAddMonoid.toAddLeftReflectLE
isOrderedAddMonoid 📖	mathematical	IsOrderedAddMonoid	IsOrderedAddMonoid addCommMonoid preorder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
isOrderedCancelMonoid 📖	mathematical	IsOrderedCancelMonoid	IsOrderedCancelMonoid commMonoid preorder	—	isOrderedMonoid IsOrderedCancelMonoid.toIsOrderedMonoid le_of_mul_le_mul_left' IsOrderedCancelMonoid.toMulLeftReflectLE
isOrderedMonoid 📖	mathematical	IsOrderedMonoid	IsOrderedMonoid commMonoid preorder	—	mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono
isOrderedRing 📖	mathematical	IsOrderedRing	IsOrderedRing semiring partialOrder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid zero_le_one IsOrderedRing.toZeroLEOneClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono
mulSingle_le_mulSingle 📖	mathematical	—	hasLe Preorder.toLE mulSingle	—	—
mulSingle_le_one 📖	mathematical	—	hasLe Preorder.toLE mulSingle instOne	—	—
one_le_mulSingle 📖	mathematical	—	hasLe Preorder.toLE instOne mulSingle	—	—
one_lt_mulSingle 📖	mathematical	—	Preorder.toLT preorder instOne mulSingle	—	—
single_le_single 📖	mathematical	—	hasLe Preorder.toLE single	—	update_le_update_iff'
single_nonneg 📖	mathematical	—	hasLe Preorder.toLE instZero single	—	le_update_self_iff
single_nonpos 📖	mathematical	—	hasLe Preorder.toLE single instZero	—	update_le_self_iff
single_pos 📖	mathematical	—	Preorder.toLT preorder instZero single	—	lt_update_self_iff

---

← Back to Index