Documentation Verification Report

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`, `single_le_single`, `single_nonneg`, `single_nonpos`	31
Total	31

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` `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` `Pi.instZero`	—	—
`const_nonpos` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `Pi.instZero`	—	`const_le_const`
`const_nonpos_of_nonpos` 📖	mathematical	`Preorder.toLE`	`Pi.hasLe` `Pi.instZero`	—	—
`const_pos` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `Pi.instZero`	—	`const_lt_const`
`extend_le_one` 📖	mathematical	`Pi.hasLe` `Pi.instOne`	`extend`	—	`dite_le_one`
`extend_nonneg` 📖	mathematical	`Pi.hasLe` `Pi.instZero`	`extend`	—	`dite_nonneg`
`extend_nonpos` 📖	mathematical	`Pi.hasLe` `Pi.instZero`	`extend`	—	`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` `Pi.instOne`	—	—
`one_le_extend` 📖	mathematical	`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`	`instAdd` `hasLe`	—	`ExistsAddOfLE.exists_add_of_le`
`existsMulOfLe` 📖	mathematical	`ExistsMulOfLE`	`instMul` `hasLe`	—	`ExistsMulOfLE.exists_mul_of_le`
`instCanonicallyOrderedAddForall` 📖	mathematical	`CanonicallyOrderedAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder`	`instAdd` `hasLe`	—	`existsAddOfLe` `CanonicallyOrderedAdd.toExistsAddOfLE` `le_add_self` `le_self_add`
`instCanonicallyOrderedMulForall` 📖	mathematical	`CanonicallyOrderedMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder`	`instMul` `hasLe`	—	`existsMulOfLe` `CanonicallyOrderedMul.toExistsMulOfLE` `le_mul_self` `le_self_mul`
`isOrderedAddCancelMonoid` 📖	mathematical	`IsOrderedCancelAddMonoid`	`addCommMonoid` `partialOrder`	—	`isOrderedAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isOrderedAddMonoid` 📖	mathematical	`IsOrderedAddMonoid`	`addCommMonoid` `partialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`isOrderedCancelMonoid` 📖	mathematical	`IsOrderedCancelMonoid`	`commMonoid` `partialOrder`	—	`isOrderedMonoid` `IsOrderedCancelMonoid.toIsOrderedMonoid` `le_of_mul_le_mul_left'` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT`
`isOrderedMonoid` 📖	mathematical	`IsOrderedMonoid`	`commMonoid` `partialOrder`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`isOrderedRing` 📖	mathematical	`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`	—	—
`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`

---

← Back to Index