Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Order/Monoid/Basic.lean

Statistics

Metric	Count
Definitions `addLeft`, `addRight`, `mulLeft`, `mulRight`	4
Theorems `isOrderedAddMonoid`, `isOrderedCancelAddMonoid`, `isOrderedCancelMonoid`, `isOrderedMonoid`, `addLeft_apply`, `addRight_apply`, `mulLeft_apply`, `mulRight_apply`, `isOrderedAddCancelMonoid`, `isOrderedAddMonoid`, `isOrderedCancelMonoid`, `isOrderedMonoid`	12
Total	16

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedAddMonoid` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder`	`IsOrderedAddMonoid`	—	`le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `le_refl`
`isOrderedCancelAddMonoid` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder`	`IsOrderedCancelAddMonoid`	—	`isOrderedAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isOrderedCancelMonoid` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder`	`IsOrderedCancelMonoid`	—	`isOrderedMonoid` `IsOrderedCancelMonoid.toIsOrderedMonoid` `mul_le_mul_iff_left` `IsOrderedMonoid.toMulLeftMono` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT`
`isOrderedMonoid` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Preorder.toLE` `PartialOrder.toPreorder`	`IsOrderedMonoid`	—	`le_imp_le_of_le_of_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `le_refl`

OrderEmbedding

Definitions

Name	Category	Theorems
`addLeft` 📖	CompOp	1 math math: `addLeft_apply`
`addRight` 📖	CompOp	1 math math: `addRight_apply`
`mulLeft` 📖	CompOp	1 math math: `mulLeft_apply`
`mulRight` 📖	CompOp	1 math math: `mulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `addLeft`	—	—
`addRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `addRight`	—	—
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `mulLeft`	—	—
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `RelEmbedding.instFunLike` `mulRight`	—	—

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedAddCancelMonoid` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`IsOrderedCancelAddMonoid`	—	`isOrderedAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `le_iff_le` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isOrderedAddMonoid` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`IsOrderedAddMonoid`	—	`Function.Injective.isOrderedAddMonoid` `le_iff_le`
`isOrderedCancelMonoid` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`IsOrderedCancelMonoid`	—	`isOrderedMonoid` `IsOrderedCancelMonoid.toIsOrderedMonoid` `le_iff_le` `IsOrderedMonoid.toMulLeftMono` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT`
`isOrderedMonoid` 📖	mathematical	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`IsOrderedMonoid`	—	`Function.Injective.isOrderedMonoid` `le_iff_le`

---

← Back to Index