Products of ordered commutative groups. #
theorem
Prod.instOrderedAddCommGroup.proof_1
{G : Type u_1}
{H : Type u_2}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
(a : G × H)
(b : G × H)
:
instance
Prod.instOrderedAddCommGroup
{G : Type u_2}
{H : Type u_3}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (G × H)
Equations
- Prod.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯
instance
Prod.instOrderedCommGroup
{G : Type u_2}
{H : Type u_3}
[OrderedCommGroup G]
[OrderedCommGroup H]
:
OrderedCommGroup (G × H)
Equations
- Prod.instOrderedCommGroup = OrderedCommGroup.mk ⋯
theorem
Prod.Lex.orderedAddCommGroup.proof_1
{G : Type u_2}
{H : Type u_1}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
instance
Prod.Lex.orderedAddCommGroup
{G : Type u_2}
{H : Type u_3}
[OrderedAddCommGroup G]
[OrderedAddCommGroup H]
:
OrderedAddCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯
instance
Prod.Lex.orderedCommGroup
{G : Type u_2}
{H : Type u_3}
[OrderedCommGroup G]
[OrderedCommGroup H]
:
OrderedCommGroup (Lex (G × H))
Equations
- Prod.Lex.orderedCommGroup = OrderedCommGroup.mk ⋯
theorem
Prod.Lex.linearOrderedAddCommGroup.proof_5
{G : Type u_2}
{H : Type u_1}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
(a : Lex (G × H))
(b : Lex (G × H))
:
compare a b = compareOfLessAndEq a b
instance
Prod.Lex.linearOrderedAddCommGroup
{G : Type u_2}
{H : Type u_3}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
:
LinearOrderedAddCommGroup (Lex (G × H))
Equations
- Prod.Lex.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
theorem
Prod.Lex.linearOrderedAddCommGroup.proof_1
{G : Type u_2}
{H : Type u_1}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
:
theorem
Prod.Lex.linearOrderedAddCommGroup.proof_4
{G : Type u_2}
{H : Type u_1}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
(a : Lex (G × H))
(b : Lex (G × H))
:
theorem
Prod.Lex.linearOrderedAddCommGroup.proof_2
{G : Type u_2}
{H : Type u_1}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
(a : Lex (G × H))
(b : Lex (G × H))
:
theorem
Prod.Lex.linearOrderedAddCommGroup.proof_3
{G : Type u_2}
{H : Type u_1}
[LinearOrderedAddCommGroup G]
[LinearOrderedAddCommGroup H]
(a : Lex (G × H))
(b : Lex (G × H))
:
instance
Prod.Lex.linearOrderedCommGroup
{G : Type u_2}
{H : Type u_3}
[LinearOrderedCommGroup G]
[LinearOrderedCommGroup H]
:
LinearOrderedCommGroup (Lex (G × H))
Equations
- Prod.Lex.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯