Documentation Verification Report

OrderDual

📁 Source: Mathlib/Algebra/Order/Monoid/Unbundled/OrderDual.lean

Statistics

Metric	Count
Definitions	0
Theorems `addLeftMono`, `addLeftReflectLE`, `addLeftReflectLT`, `addLeftStrictMono`, `addRightMono`, `addRightReflectLE`, `addRightReflectLT`, `addRightStrictMono`, `mulLeftMono`, `mulLeftReflectLE`, `mulLeftReflectLT`, `mulLeftStrictMono`, `mulRightMono`, `mulRightReflectLE`, `mulRightReflectLT`, `mulRightStrictMono`	16
Total	16

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	—	`AddLeftMono` `OrderDual` `instAddOrderDual` `instLE`	—	`Covariant.flip` `CovariantClass.elim`
`addLeftReflectLE` 📖	mathematical	—	`AddLeftReflectLE` `OrderDual` `instAddOrderDual` `instLE`	—	`Contravariant.flip` `ContravariantClass.elim`
`addLeftReflectLT` 📖	mathematical	—	`AddLeftReflectLT` `OrderDual` `instAddOrderDual` `instLT`	—	`Contravariant.flip` `ContravariantClass.elim`
`addLeftStrictMono` 📖	mathematical	—	`AddLeftStrictMono` `OrderDual` `instAddOrderDual` `instLT`	—	`Covariant.flip` `CovariantClass.elim`
`addRightMono` 📖	mathematical	—	`AddRightMono` `OrderDual` `instAddOrderDual` `instLE`	—	`Covariant.flip` `CovariantClass.elim`
`addRightReflectLE` 📖	mathematical	—	`AddRightReflectLE` `OrderDual` `instAddOrderDual` `instLE`	—	`Contravariant.flip` `ContravariantClass.elim`
`addRightReflectLT` 📖	mathematical	—	`AddRightReflectLT` `OrderDual` `instAddOrderDual` `instLT`	—	`Contravariant.flip` `ContravariantClass.elim`
`addRightStrictMono` 📖	mathematical	—	`AddRightStrictMono` `OrderDual` `instAddOrderDual` `instLT`	—	`Covariant.flip` `CovariantClass.elim`
`mulLeftMono` 📖	mathematical	—	`MulLeftMono` `OrderDual` `instMulOrderDual` `instLE`	—	`Covariant.flip` `CovariantClass.elim`
`mulLeftReflectLE` 📖	mathematical	—	`MulLeftReflectLE` `OrderDual` `instMulOrderDual` `instLE`	—	`Contravariant.flip` `ContravariantClass.elim`
`mulLeftReflectLT` 📖	mathematical	—	`MulLeftReflectLT` `OrderDual` `instMulOrderDual` `instLT`	—	`Contravariant.flip` `ContravariantClass.elim`
`mulLeftStrictMono` 📖	mathematical	—	`MulLeftStrictMono` `OrderDual` `instMulOrderDual` `instLT`	—	`Covariant.flip` `CovariantClass.elim`
`mulRightMono` 📖	mathematical	—	`MulRightMono` `OrderDual` `instMulOrderDual` `instLE`	—	`Covariant.flip` `CovariantClass.elim`
`mulRightReflectLE` 📖	mathematical	—	`MulRightReflectLE` `OrderDual` `instMulOrderDual` `instLE`	—	`Contravariant.flip` `ContravariantClass.elim`
`mulRightReflectLT` 📖	mathematical	—	`MulRightReflectLT` `OrderDual` `instMulOrderDual` `instLT`	—	`Contravariant.flip` `ContravariantClass.elim`
`mulRightStrictMono` 📖	mathematical	—	`MulRightStrictMono` `OrderDual` `instMulOrderDual` `instLT`	—	`Covariant.flip` `CovariantClass.elim`

---

← Back to Index