Products of ordered commutative groups. #
instance
Prod.instOrderedAddCommGroupSum
{G : Type u_1}
{H : Type u_2}
[inst : OrderedAddCommGroup G]
[inst : OrderedAddCommGroup H]
:
OrderedAddCommGroup (G × H)
Equations
- One or more equations did not get rendered due to their size.
def
Prod.instOrderedAddCommGroupSum.proof_2
{G : Type u_1}
{H : Type u_2}
[inst : OrderedAddCommGroup G]
[inst : OrderedAddCommGroup H]
(a : G × H)
(b : G × H)
:
instance
Prod.instOrderedCommGroupProd
{G : Type u_1}
{H : Type u_2}
[inst : OrderedCommGroup G]
[inst : OrderedCommGroup H]
:
OrderedCommGroup (G × H)
Equations
- One or more equations did not get rendered due to their size.