Products of ordered commutative groups. #
instance
Prod.instOrderedCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedCommGroup G]
[OrderedCommGroup H]
:
OrderedCommGroup (G × H)
Equations
- Prod.instOrderedCommGroup = { toCommGroup := Prod.instCommGroup, toPartialOrder := Prod.instPartialOrder G H, mul_le_mul_left := ⋯ }
instance
Prod.instOrderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (G × H)
Equations
- Prod.instOrderedAddCommGroup = { toAddCommGroup := Prod.instAddCommGroup, toPartialOrder := Prod.instPartialOrder G H, add_le_add_left := ⋯ }
instance
Prod.Lex.orderedCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedCommGroup G]
[OrderedCommGroup H]
:
OrderedCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedCommGroup = { toCommGroup := instCommGroupLex, toPartialOrder := Prod.Lex.partialOrder G H, mul_le_mul_left := ⋯ }
instance
Prod.Lex.orderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedAddCommGroup = { toAddCommGroup := instAddCommGroupLex, toPartialOrder := Prod.Lex.partialOrder G H, add_le_add_left := ⋯ }
instance
Prod.Lex.linearOrderedCommGroup
{G : Type u_1}
{H : Type u_2}
[LinearOrderedCommGroup G]
[LinearOrderedCommGroup H]
:
LinearOrderedCommGroup (Lex (G × H))
Equations
- One or more equations did not get rendered due to their size.
instance
Prod.Lex.linearOrderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
:
LinearOrderedAddCommGroup (Lex (G × H))
Equations
- One or more equations did not get rendered due to their size.