Documentation
Mathlib
.
Algebra
.
Order
.
Group
.
TypeTags
Search
return to top
source
Imports
Init
Mathlib.Algebra.Order.Group.Defs
Mathlib.Algebra.Order.Monoid.TypeTags
Imported by
Multiplicative
.
orderedCommGroup
Additive
.
orderedAddCommGroup
Multiplicative
.
linearOrderedCommGroup
Additive
.
linearOrderedAddCommGroup
Ordered group structures on
Multiplicative
α
and
Additive
α
.
#
source
instance
Multiplicative
.
orderedCommGroup
{α :
Type
u_1}
[
OrderedAddCommGroup
α
]
:
OrderedCommGroup
(
Multiplicative
α
)
Equations
Multiplicative.orderedCommGroup
=
OrderedCommGroup.mk
⋯
source
instance
Additive
.
orderedAddCommGroup
{α :
Type
u_1}
[
OrderedCommGroup
α
]
:
OrderedAddCommGroup
(
Additive
α
)
Equations
Additive.orderedAddCommGroup
=
OrderedAddCommGroup.mk
⋯
source
instance
Multiplicative
.
linearOrderedCommGroup
{α :
Type
u_1}
[
LinearOrderedAddCommGroup
α
]
:
LinearOrderedCommGroup
(
Multiplicative
α
)
Equations
Multiplicative.linearOrderedCommGroup
=
LinearOrderedCommGroup.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯
source
instance
Additive
.
linearOrderedAddCommGroup
{α :
Type
u_1}
[
LinearOrderedCommGroup
α
]
:
LinearOrderedAddCommGroup
(
Additive
α
)
Equations
Additive.linearOrderedAddCommGroup
=
LinearOrderedAddCommGroup.mk
⋯
LinearOrder.decidableLE
LinearOrder.decidableEq
LinearOrder.decidableLT
⋯
⋯
⋯