Documentation Verification Report

Order

📁 Source: Mathlib/GroupTheory/MonoidLocalization/Order.lean

Statistics

Metric	Count
Definitions `decidableLE`, `decidableLT`, `instLinearAddOrderOfIsOrderedAddCancelMonoid`, `le`, `lt`, `mkOrderEmbedding`, `partialOrder`, `decidableLE`, `decidableLT`, `instLinearOrderOfIsOrderedCancelMonoid`, `le`, `lt`, `mkOrderEmbedding`, `partialOrder`	14
Theorems `isOrderedAddCancelMonoid`, `mkOrderEmbedding_apply`, `mk_le_mk`, `mk_lt_mk`, `isOrderedCancelMonoid`, `mkOrderEmbedding_apply`, `mk_le_mk`, `mk_lt_mk`	8
Total	22

AddLocalization

Definitions

Name	Category	Theorems
`decidableLE` 📖	CompOp	—
`decidableLT` 📖	CompOp	—
`instLinearAddOrderOfIsOrderedAddCancelMonoid` 📖	CompOp	—
`le` 📖	CompOp	2 math math: `mkOrderEmbedding_apply`, `mk_le_mk`
`lt` 📖	CompOp	1 math math: `mk_lt_mk`
`mkOrderEmbedding` 📖	CompOp	1 math math: `mkOrderEmbedding_apply`
`partialOrder` 📖	CompOp	1 math math: `isOrderedAddCancelMonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedAddCancelMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `AddLocalization` `AddOreLocalization.instAddCommMonoid` `AddOreLocalization.addOreSetComm` `partialOrder`	—	`induction_on₂` `induction_on` `mk_add` `add_add_add_comm` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `induction_on₃` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`mkOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `AddLocalization` `Preorder.toLE` `PartialOrder.toPreorder` `le` `RelEmbedding.instFunLike` `mkOrderEmbedding`	—	—
`mk_le_mk` 📖	mathematical	—	`AddLocalization` `le` `Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	—	—
`mk_lt_mk` 📖	mathematical	—	`AddLocalization` `lt` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike`	—	—

Localization

Definitions

Name	Category	Theorems
`decidableLE` 📖	CompOp	—
`decidableLT` 📖	CompOp	—
`instLinearOrderOfIsOrderedCancelMonoid` 📖	CompOp	—
`le` 📖	CompOp	2 math math: `mk_le_mk`, `mkOrderEmbedding_apply`
`lt` 📖	CompOp	1 math math: `mk_lt_mk`
`mkOrderEmbedding` 📖	CompOp	1 math math: `mkOrderEmbedding_apply`
`partialOrder` 📖	CompOp	1 math math: `isOrderedCancelMonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOrderedCancelMonoid` 📖	mathematical	—	`IsOrderedCancelMonoid` `Localization` `OreLocalization.instCommMonoid` `OreLocalization.oreSetComm` `partialOrder`	—	`induction_on₂` `induction_on` `mk_mul` `mul_mul_mul_comm` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsOrderedCancelMonoid.toIsOrderedMonoid` `induction_on₃` `le_of_mul_le_mul_left'` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `IsCancelMul.toIsLeftCancelMul` `IsOrderedCancelMonoid.toIsCancelMul` `IsOrderedCancelMonoid.toMulLeftReflectLT`
`mkOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Localization` `Preorder.toLE` `PartialOrder.toPreorder` `le` `RelEmbedding.instFunLike` `mkOrderEmbedding`	—	—
`mk_le_mk` 📖	mathematical	—	`Localization` `le` `Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	—	—
`mk_lt_mk` 📖	mathematical	—	`Localization` `lt` `Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike`	—	—

---

← Back to Index