Documentation
Mathlib
.
Algebra
.
Order
.
Monoid
.
OrderDual
Search
return to top
source
Imports
Init
Mathlib.Algebra.Order.Group.Synonym
Mathlib.Algebra.Order.Monoid.Defs
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
Imported by
OrderDual
.
orderedCommMonoid
OrderDual
.
orderedAddCommMonoid
OrderDual
.
OrderedCancelCommMonoid
.
to_mulLeftReflectLE
OrderDual
.
OrderedCancelAddCommMonoid
.
to_mulLeftReflectLE
OrderDual
.
orderedCancelCommMonoid
OrderDual
.
orderedAddCancelCommMonoid
OrderDual
.
linearOrderedCancelCommMonoid
OrderDual
.
linearOrderedAddCancelCommMonoid
OrderDual
.
linearOrderedCommMonoid
OrderDual
.
linearOrderedAddCommMonoid
Ordered monoid structures on the order dual.
#
source
instance
OrderDual
.
orderedCommMonoid
{α :
Type
u}
[
OrderedCommMonoid
α
]
:
OrderedCommMonoid
α
ᵒᵈ
Equations
OrderDual.orderedCommMonoid
=
OrderedCommMonoid.mk
⋯
source
instance
OrderDual
.
orderedAddCommMonoid
{α :
Type
u}
[
OrderedAddCommMonoid
α
]
:
OrderedAddCommMonoid
α
ᵒᵈ
Equations
OrderDual.orderedAddCommMonoid
=
OrderedAddCommMonoid.mk
⋯
source
instance
OrderDual
.
OrderedCancelCommMonoid
.
to_mulLeftReflectLE
{α :
Type
u}
[
OrderedCancelCommMonoid
α
]
:
MulLeftReflectLE
α
ᵒᵈ
source
instance
OrderDual
.
OrderedCancelAddCommMonoid
.
to_mulLeftReflectLE
{α :
Type
u}
[
OrderedCancelAddCommMonoid
α
]
:
AddLeftReflectLE
α
ᵒᵈ
source
instance
OrderDual
.
orderedCancelCommMonoid
{α :
Type
u}
[
OrderedCancelCommMonoid
α
]
:
OrderedCancelCommMonoid
α
ᵒᵈ
Equations
OrderDual.orderedCancelCommMonoid
=
OrderedCancelCommMonoid.mk
⋯
source
instance
OrderDual
.
orderedAddCancelCommMonoid
{α :
Type
u}
[
OrderedCancelAddCommMonoid
α
]
:
OrderedCancelAddCommMonoid
α
ᵒᵈ
Equations
OrderDual.orderedAddCancelCommMonoid
=
OrderedCancelAddCommMonoid.mk
⋯
source
instance
OrderDual
.
linearOrderedCancelCommMonoid
{α :
Type
u}
[
LinearOrderedCancelCommMonoid
α
]
:
LinearOrderedCancelCommMonoid
α
ᵒᵈ
Equations
OrderDual.linearOrderedCancelCommMonoid
=
LinearOrderedCancelCommMonoid.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯
source
instance
OrderDual
.
linearOrderedAddCancelCommMonoid
{α :
Type
u}
[
LinearOrderedCancelAddCommMonoid
α
]
:
LinearOrderedCancelAddCommMonoid
α
ᵒᵈ
Equations
OrderDual.linearOrderedAddCancelCommMonoid
=
LinearOrderedCancelAddCommMonoid.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯
source
instance
OrderDual
.
linearOrderedCommMonoid
{α :
Type
u}
[
LinearOrderedCommMonoid
α
]
:
LinearOrderedCommMonoid
α
ᵒᵈ
Equations
OrderDual.linearOrderedCommMonoid
=
LinearOrderedCommMonoid.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯
source
instance
OrderDual
.
linearOrderedAddCommMonoid
{α :
Type
u}
[
LinearOrderedAddCommMonoid
α
]
:
LinearOrderedAddCommMonoid
α
ᵒᵈ
Equations
OrderDual.linearOrderedAddCommMonoid
=
LinearOrderedAddCommMonoid.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯