Documentation
Mathlib
.
Algebra
.
Order
.
Group
.
TypeTags
Search
Google site search
Mathlib
.
Algebra
.
Order
.
Group
.
TypeTags
source
Imports
Init
Mathlib.Algebra.Order.Group.Instances
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
α
)
source
instance
Additive
.
orderedAddCommGroup
{α :
Type
u_1}
[
OrderedCommGroup
α
]
:
OrderedAddCommGroup
(
Additive
α
)
source
instance
Multiplicative
.
linearOrderedCommGroup
{α :
Type
u_1}
[
LinearOrderedAddCommGroup
α
]
:
LinearOrderedCommGroup
(
Multiplicative
α
)
source
instance
Additive
.
linearOrderedAddCommGroup
{α :
Type
u_1}
[
LinearOrderedCommGroup
α
]
:
LinearOrderedAddCommGroup
(
Additive
α
)