OrderedMonoid

Statistics

Metric	Count
Definitions	0
Theorems `instCanonicallyOrderedAdd`, `instIsOrderedCancelAddMonoid`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instCanonicallyOrderedAdd` 📖	mathematical	—	`CanonicallyOrderedAdd` `Multiset` `instAdd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`ExistsAddOfLE.exists_add_of_le` `instExistsAddOfLE` `le_add_left` `le_add_right`
`instIsOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `Multiset` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `instPartialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `instAddLeftMono` `le_of_add_le_add_left` `instAddLeftReflectLE`

---