Ordered monoids #
This file develops some additional material on ordered monoids.
Pullback an OrderedCommMonoid
under an injective map.
See note [reducible non-instances].
Instances For
Pullback an OrderedAddCommMonoid
under an injective map.
Instances For
Pullback an OrderedCancelCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
Instances For
Pullback an OrderedCancelAddCommMonoid
under an injective map.
Equations
Instances For
Pullback a LinearOrderedCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
Instances For
Pullback an OrderedAddCommMonoid
under an injective map.
Equations
Instances For
Pullback a LinearOrderedCancelCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pullback a LinearOrderedCancelAddCommMonoid
under an injective map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The order embedding sending b
to a * b
, for some fixed a
.
See also OrderIso.mulLeft
when working in an ordered group.
Instances For
The order embedding sending b
to a + b
, for some fixed a
.
See also OrderIso.addLeft
when working in an additive ordered group.
Instances For
The order embedding sending b
to b * a
, for some fixed a
.
See also OrderIso.mulRight
when working in an ordered group.
Instances For
The order embedding sending b
to b + a
, for some fixed a
.
See also OrderIso.addRight
when working in an additive ordered group.