Documentation Verification Report

Opposite

📁 Source: Mathlib/Algebra/Order/Group/Opposite.lean

Statistics

Metric	Count
Definitions `instPartialOrder`, `instPreorder`, `instPartialOrder`, `instPreorder`	4
Theorems `instIsOrderedAddMonoid`, `instIsOrderedMonoid`, `nonneg_op`, `nonneg_unop`, `one_le_op`, `one_le_unop`, `op_le_one`, `op_le_op`, `op_nonpos`, `unop_le_one`, `unop_le_unop`, `unop_nonpos`, `instIsOrderedAddMonoid`, `instIsOrderedMonoid`, `one_le_op`, `one_le_unop`, `op_le_one`, `op_le_op`, `op_nonneg`, `op_nonpos`, `unop_le_one`, `unop_le_unop`, `unop_nonneg`, `unop_nonpos`	24
Total	28

AddOpposite

Definitions

Name	Category	Theorems
`instPartialOrder` 📖	CompOp	3 math math: `instIsOrderedRing`, `instIsOrderedAddMonoid`, `instIsOrderedMonoid`
`instPreorder` 📖	CompOp	10 math math: `op_le_one`, `one_le_op`, `unop_nonpos`, `op_nonpos`, `nonneg_op`, `one_le_unop`, `nonneg_unop`, `unop_le_one`, `op_le_op`, `unop_le_unop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `AddOpposite` `instAddCommMonoid` `instPartialOrder`	—	`add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `unop_le_unop`
`instIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `AddOpposite` `instCommMonoid` `instPartialOrder`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`nonneg_op` 📖	mathematical	—	`AddOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `op`	—	—
`nonneg_unop` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `unop` `AddOpposite` `instPreorder` `instZero`	—	—
`one_le_op` 📖	mathematical	—	`AddOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `op`	—	—
`one_le_unop` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `unop` `AddOpposite` `instPreorder` `instOne`	—	—
`op_le_one` 📖	mathematical	—	`AddOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `op` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—
`op_le_op` 📖	mathematical	—	`AddOpposite` `Preorder.toLE` `instPreorder` `op`	—	—
`op_nonpos` 📖	mathematical	—	`AddOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `op` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`unop_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `unop` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddOpposite` `instPreorder` `instOne`	—	—
`unop_le_unop` 📖	mathematical	—	`Preorder.toLE` `unop` `AddOpposite` `instPreorder`	—	—
`unop_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `unop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddOpposite` `instPreorder` `instZero`	—	—

MulOpposite

Definitions

Name	Category	Theorems
`instPartialOrder` 📖	CompOp	4 math math: `instStarOrderedRing`, `instIsOrderedMonoid`, `instIsOrderedAddMonoid`, `instIsOrderedRing`
`instPreorder` 📖	CompOp	10 math math: `one_le_op`, `op_le_op`, `one_le_unop`, `op_nonpos`, `unop_le_unop`, `unop_nonpos`, `op_nonneg`, `unop_le_one`, `op_le_one`, `unop_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `MulOpposite` `instAddCommMonoid` `instPartialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`instIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `MulOpposite` `instCommMonoid` `instPartialOrder`	—	`mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono`
`one_le_op` 📖	mathematical	—	`MulOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `op`	—	—
`one_le_unop` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `unop` `MulOpposite` `instPreorder` `instOne`	—	—
`op_le_one` 📖	mathematical	—	`MulOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `op` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—
`op_le_op` 📖	mathematical	—	`MulOpposite` `Preorder.toLE` `instPreorder` `op`	—	—
`op_nonneg` 📖	mathematical	—	`MulOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `op`	—	—
`op_nonpos` 📖	mathematical	—	`MulOpposite` `Preorder.toLE` `instPreorder` `PartialOrder.toPreorder` `op` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`unop_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `unop` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOpposite` `instPreorder` `instOne`	—	—
`unop_le_unop` 📖	mathematical	—	`Preorder.toLE` `unop` `MulOpposite` `instPreorder`	—	—
`unop_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `unop` `MulOpposite` `instPreorder` `instZero`	—	—
`unop_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `unop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MulOpposite` `instPreorder` `instZero`	—	—

---

← Back to Index