Documentation Verification Report

AddTorsor

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

Statistics

Metric	Count
Definitions `IsOrderedCancelSMul`, `IsOrderedCancelVAdd`, `IsOrderedSMul`, `IsOrderedVAdd`	4
Theorems `le_of_smul_le_smul_left`, `le_of_smul_le_smul_right`, `toIsOrderedSMul`, `le_of_vadd_le_vadd_left`, `le_of_vadd_le_vadd_right`, `toIsOrderedVAdd`, `smul_le_smul`, `smul_le_smul_left`, `smul_le_smul_right`, `vadd_le_vadd`, `vadd_le_vadd_left`, `vadd_le_vadd_right`, `smul`, `vadd`, `smul_lt_smul_of_le_of_lt`, `smul_lt_smul_of_lt_of_le`, `vadd_lt_vadd_of_le_of_lt`, `vadd_lt_vadd_of_lt_of_le`, `instContravariantClassHSMulLeOfIsOrderedCancelSMul`, `instContravariantClassHVAddLeOfIsOrderedCancelVAdd`, `instCovariantClassHSMulLeOfIsOrderedSMul`, `instCovariantClassHVAddLeOfIsOrderedVAdd`, `instIsCancelSMulOfIsOrderedCancelSMul`, `instIsCancelVAddOfIsOrderedCancelVAdd`, `instIsOrderedCancelSMulOfIsOrderedCancelMonoid`, `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`, `instIsOrderedSMulOfIsOrderedMonoid`, `instIsOrderedVAddOfIsOrderedAddMonoid`	28
Total	32

IsOrderedCancelSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_smul_le_smul_left` 📖	—	—	—	—	—
`le_of_smul_le_smul_right` 📖	—	—	—	—	—
`toIsOrderedSMul` 📖	mathematical	—	`IsOrderedSMul`	—	—

IsOrderedCancelVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_of_vadd_le_vadd_left` 📖	—	`HVAdd.hVAdd` `instHVAdd`	—	—	—
`le_of_vadd_le_vadd_right` 📖	—	`HVAdd.hVAdd` `instHVAdd`	—	—	—
`toIsOrderedVAdd` 📖	mathematical	—	`IsOrderedVAdd`	—	—

IsOrderedSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_le_smul` 📖	—	`Preorder.toLE`	—	—	`LE.le.trans` `smul_le_smul_left` `smul_le_smul_right`
`smul_le_smul_left` 📖	—	—	—	—	—
`smul_le_smul_right` 📖	—	—	—	—	—

IsOrderedVAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vadd_le_vadd` 📖	mathematical	`Preorder.toLE`	`HVAdd.hVAdd` `instHVAdd`	—	`LE.le.trans` `vadd_le_vadd_left` `vadd_le_vadd_right`
`vadd_le_vadd_left` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd`	—	—
`vadd_le_vadd_right` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd`	—	—

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	—	`Monotone`	—	—	`LE.le.trans` `IsOrderedSMul.smul_le_smul_left` `IsOrderedSMul.smul_le_smul_right`
`vadd` 📖	mathematical	`Monotone`	`HVAdd.hVAdd` `instHVAdd`	—	`LE.le.trans` `IsOrderedVAdd.vadd_le_vadd_left` `IsOrderedVAdd.vadd_le_vadd_right`

SMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_lt_smul_of_le_of_lt` 📖	—	`Preorder.toLT`	—	—	`lt_of_le_of_lt` `IsOrderedSMul.smul_le_smul_right` `IsOrderedCancelSMul.toIsOrderedSMul` `lt_of_le_not_ge` `IsOrderedSMul.smul_le_smul_left` `le_of_lt` `IsOrderedCancelSMul.le_of_smul_le_smul_left` `lt_iff_le_not_ge`
`smul_lt_smul_of_lt_of_le` 📖	—	`Preorder.toLT` `Preorder.toLE`	—	—	`lt_of_le_of_lt` `IsOrderedSMul.smul_le_smul_left` `IsOrderedCancelSMul.toIsOrderedSMul` `lt_of_le_not_ge` `IsOrderedSMul.smul_le_smul_right` `le_of_lt` `IsOrderedCancelSMul.le_of_smul_le_smul_right` `lt_iff_le_not_ge`

VAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vadd_lt_vadd_of_le_of_lt` 📖	mathematical	`Preorder.toLT`	`HVAdd.hVAdd` `instHVAdd`	—	`lt_of_le_of_lt` `IsOrderedVAdd.vadd_le_vadd_right` `IsOrderedCancelVAdd.toIsOrderedVAdd` `lt_of_le_not_ge` `IsOrderedVAdd.vadd_le_vadd_left` `le_of_lt` `IsOrderedCancelVAdd.le_of_vadd_le_vadd_left` `lt_iff_le_not_ge`
`vadd_lt_vadd_of_lt_of_le` 📖	mathematical	`Preorder.toLT` `Preorder.toLE`	`HVAdd.hVAdd` `instHVAdd`	—	`lt_of_le_of_lt` `IsOrderedVAdd.vadd_le_vadd_left` `IsOrderedCancelVAdd.toIsOrderedVAdd` `lt_of_le_not_ge` `IsOrderedVAdd.vadd_le_vadd_right` `le_of_lt` `IsOrderedCancelVAdd.le_of_vadd_le_vadd_right` `lt_iff_le_not_ge`

(root)

Definitions

Name	Category	Theorems
`IsOrderedCancelSMul` 📖	CompData	1 math math: `instIsOrderedCancelSMulOfIsOrderedCancelMonoid`
`IsOrderedCancelVAdd` 📖	CompData	1 math math: `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`
`IsOrderedSMul` 📖	CompData	2 math math: `IsOrderedCancelSMul.toIsOrderedSMul`, `instIsOrderedSMulOfIsOrderedMonoid`
`IsOrderedVAdd` 📖	CompData	2 math math: `instIsOrderedVAddOfIsOrderedAddMonoid`, `IsOrderedCancelVAdd.toIsOrderedVAdd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContravariantClassHSMulLeOfIsOrderedCancelSMul` 📖	mathematical	—	`ContravariantClass`	—	`IsOrderedCancelSMul.le_of_smul_le_smul_left`
`instContravariantClassHVAddLeOfIsOrderedCancelVAdd` 📖	mathematical	—	`ContravariantClass` `HVAdd.hVAdd` `instHVAdd`	—	`IsOrderedCancelVAdd.le_of_vadd_le_vadd_left`
`instCovariantClassHSMulLeOfIsOrderedSMul` 📖	mathematical	—	`CovariantClass`	—	`IsOrderedSMul.smul_le_smul_left`
`instCovariantClassHVAddLeOfIsOrderedVAdd` 📖	mathematical	—	`CovariantClass` `HVAdd.hVAdd` `instHVAdd`	—	`IsOrderedVAdd.vadd_le_vadd_left`
`instIsCancelSMulOfIsOrderedCancelSMul` 📖	mathematical	—	`IsCancelSMul`	—	`LE.le.antisymm` `IsOrderedCancelSMul.le_of_smul_le_smul_left` `Eq.le` `Eq.ge` `IsOrderedCancelSMul.le_of_smul_le_smul_right`
`instIsCancelVAddOfIsOrderedCancelVAdd` 📖	mathematical	—	`IsCancelVAdd`	—	`LE.le.antisymm` `IsOrderedCancelVAdd.le_of_vadd_le_vadd_left` `Eq.le` `Eq.ge` `IsOrderedCancelVAdd.le_of_vadd_le_vadd_right`
`instIsOrderedCancelSMulOfIsOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelSMul` `Preorder.toLE` `PartialOrder.toPreorder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`instIsOrderedSMulOfIsOrderedMonoid` `IsOrderedCancelMonoid.toIsOrderedMonoid` `le_of_mul_le_mul_left'` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT` `le_of_mul_le_mul_right'` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `IsCancelMul.toIsRightCancelMul` `contravariant_swap_mul_of_contravariant_mul`
`instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` 📖	mathematical	—	`IsOrderedCancelVAdd` `Preorder.toLE` `PartialOrder.toPreorder` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`instIsOrderedVAddOfIsOrderedAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `le_of_add_le_add_right` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add`
`instIsOrderedSMulOfIsOrderedMonoid` 📖	mathematical	—	`IsOrderedSMul` `Preorder.toLE` `PartialOrder.toPreorder` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul`
`instIsOrderedVAddOfIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedVAdd` `Preorder.toLE` `PartialOrder.toPreorder` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `add_le_add_left` `covariant_swap_add_of_covariant_add`

---

← Back to Index