Ordered monoids #
This file develops some additional material on ordered monoids.
Pullback an OrderedCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
- Function.Injective.orderedCommMonoid f hf one mul npow = OrderedCommMonoid.mk ⋯
Instances For
Pullback an OrderedAddCommMonoid
under an injective map.
Equations
- Function.Injective.orderedAddCommMonoid f hf one mul npow = OrderedAddCommMonoid.mk ⋯
Instances For
Pullback an OrderedCancelCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
- Function.Injective.orderedCancelCommMonoid f hf one mul npow = OrderedCancelCommMonoid.mk ⋯
Instances For
Pullback an OrderedCancelAddCommMonoid
under an injective map.
Equations
- Function.Injective.orderedCancelAddCommMonoid f hf one mul npow = OrderedCancelAddCommMonoid.mk ⋯
Instances For
Pullback a LinearOrderedCommMonoid
under an injective map.
See note [reducible non-instances].
Equations
- Function.Injective.linearOrderedCommMonoid f hf one mul npow sup inf = LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
Instances For
Pullback an OrderedAddCommMonoid
under an injective map.
Equations
- Function.Injective.linearOrderedAddCommMonoid f hf one mul npow sup inf = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
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.
Equations
- OrderEmbedding.mulLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m * n) ⋯
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.
Equations
- OrderEmbedding.addLeft m = OrderEmbedding.ofStrictMono (fun (n : α) => m + n) ⋯
Instances For
The order embedding sending b
to b * a
, for some fixed a
.
See also OrderIso.mulRight
when working in an ordered group.
Equations
- OrderEmbedding.mulRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n * m) ⋯
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.
Equations
- OrderEmbedding.addRight m = OrderEmbedding.ofStrictMono (fun (n : α) => n + m) ⋯