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 = OrderedCommGroup.mk ⋯
instance
Prod.instOrderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (G × H)
Equations
- Prod.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯
instance
Prod.Lex.orderedCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedCommGroup G]
[OrderedCommGroup H]
:
OrderedCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedCommGroup = OrderedCommGroup.mk ⋯
instance
Prod.Lex.orderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯
instance
Prod.Lex.linearOrderedCommGroup
{G : Type u_1}
{H : Type u_2}
[LinearOrderedCommGroup G]
[LinearOrderedCommGroup H]
:
LinearOrderedCommGroup (Lex (G × H))
Equations
- Prod.Lex.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
instance
Prod.Lex.linearOrderedAddCommGroup
{G : Type u_1}
{H : Type u_2}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
:
LinearOrderedAddCommGroup (Lex (G × H))
Equations
- Prod.Lex.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯