Documentation

Mathlib.Algebra.Order.Group.Prod

Products of ordered commutative groups. #

source
instance Prod.instOrderedCommGroup {G : Type u_1} {H : Type u_2} [OrderedCommGroup G] [OrderedCommGroup H] :
OrderedCommGroup (G × H)
Equations
source
instance Prod.instOrderedAddCommGroup {G : Type u_1} {H : Type u_2} [OrderedAddCommGroup G] [OrderedAddCommGroup H] :
OrderedAddCommGroup (G × H)
Equations
source
instance Prod.Lex.orderedCommGroup {G : Type u_1} {H : Type u_2} [OrderedCommGroup G] [OrderedCommGroup H] :
OrderedCommGroup (Lex (G × H))
Equations
source
instance Prod.Lex.orderedAddCommGroup {G : Type u_1} {H : Type u_2} [OrderedAddCommGroup G] [OrderedAddCommGroup H] :
OrderedAddCommGroup (Lex (G × H))
Equations
source
instance Prod.Lex.linearOrderedCommGroup {G : Type u_1} {H : Type u_2} [LinearOrderedCommGroup G] [LinearOrderedCommGroup H] :
LinearOrderedCommGroup (Lex (G × H))
Equations
source
instance Prod.Lex.linearOrderedAddCommGroup {G : Type u_1} {H : Type u_2} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] :
LinearOrderedAddCommGroup (Lex (G × H))
Equations