Lexicographic product of algebraic order structures

This file proves that the lexicographic order on pi types is compatible with the pointwise algebraic operations.

instance Pi.Lex.orderedCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelCommMonoid (α i)] : OrderedCancelCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedCancelCommMonoid = { toCommMonoid := instCommMonoidLex, toPartialOrder := Pi.instPartialOrderLexForallOfLinearOrder, mul_le_mul_left := ⋯, le_of_mul_le_mul_left := ⋯ }

instance Pi.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : OrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedAddCancelCommMonoid = { toAddCommMonoid := instAddCommMonoidLex, toPartialOrder := Pi.instPartialOrderLexForallOfLinearOrder, add_le_add_left := ⋯, le_of_add_le_add_left := ⋯ }

instance Pi.Lex.orderedCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCommGroup (α i)] : OrderedCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedCommGroup = { toCommGroup := instCommGroupLex, toPartialOrder := Pi.instPartialOrderLexForallOfLinearOrder, mul_le_mul_left := ⋯ }

instance Pi.Lex.orderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (α i)] : OrderedAddCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedAddCommGroup = { toAddCommGroup := instAddCommGroupLex, toPartialOrder := Pi.instPartialOrderLexForallOfLinearOrder, add_le_add_left := ⋯ }

noncomputable instance Pi.Lex.linearOrderedCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → LinearOrderedCancelCommMonoid (α i)] : LinearOrderedCancelCommMonoid (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Pi.Lex.linearOrderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] : LinearOrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Pi.Lex.linearOrderedCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → LinearOrderedCommGroup (α i)] : LinearOrderedCommGroup (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Pi.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [WellFoundedLT ι] [(i : ι) → LinearOrderedAddCommGroup (α i)] : LinearOrderedAddCommGroup (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.