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.orderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : OrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

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

Equations

• Pi.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

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

Equations

• Pi.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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

Equations

• Pi.Lex.orderedCommGroup = OrderedCommGroup.mk ⋯

noncomputable instance Pi.Lex.linearOrderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] : LinearOrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

noncomputable instance Pi.Lex.linearOrderedCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelCommMonoid (α i)] : LinearOrderedCancelCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

noncomputable instance Pi.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] : LinearOrderedAddCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

noncomputable instance Pi.Lex.linearOrderedCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCommGroup (α i)] : LinearOrderedCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯