Documentation

@[implicit_reducible]

instance OrderDual.instOne {α : Type u_1} [h : One α] :

One αᵒᵈ

@[implicit_reducible]

instance OrderDual.instZero {α : Type u_1} [h : Zero α] :

Zero αᵒᵈ

@[implicit_reducible]

instance OrderDual.instMul {α : Type u_1} [h : Mul α] :

Mul αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAdd {α : Type u_1} [h : Add α] :

Add αᵒᵈ

@[implicit_reducible]

instance OrderDual.instInv {α : Type u_1} [h : Inv α] :

Inv αᵒᵈ

@[implicit_reducible]

instance OrderDual.instNeg {α : Type u_1} [h : Neg α] :

Neg αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDiv {α : Type u_1} [h : Div α] :

Div αᵒᵈ

@[implicit_reducible]

instance OrderDual.instSub {α : Type u_1} [h : Sub α] :

Sub αᵒᵈ

@[implicit_reducible]

instance OrderDual.instPow {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow αᵒᵈ β

@[implicit_reducible]

instance OrderDual.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd β αᵒᵈ

@[implicit_reducible]

instance OrderDual.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul β αᵒᵈ

@[implicit_reducible]

instance OrderDual.instPow_1 {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow α βᵒᵈ

@[implicit_reducible]

instance OrderDual.instVAdd' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd βᵒᵈ α

@[implicit_reducible]

instance OrderDual.instSMul' {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul βᵒᵈ α

@[implicit_reducible]

instance OrderDual.instSemigroup {α : Type u_1} [h : Semigroup α] :

Semigroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddSemigroup {α : Type u_1} [h : AddSemigroup α] :

AddSemigroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommSemigroup {α : Type u_1} [h : CommSemigroup α] :

CommSemigroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCommSemigroup {α : Type u_1} [h : AddCommSemigroup α] :

AddCommSemigroup αᵒᵈ

instance OrderDual.instIsLeftCancelMul {α : Type u_1} [Mul α] [h : IsLeftCancelMul α] :

IsLeftCancelMul αᵒᵈ

instance OrderDual.instIsLeftCancelAdd {α : Type u_1} [Add α] [h : IsLeftCancelAdd α] :

IsLeftCancelAdd αᵒᵈ

instance OrderDual.instIsRightCancelMul {α : Type u_1} [Mul α] [h : IsRightCancelMul α] :

IsRightCancelMul αᵒᵈ

instance OrderDual.instIsRightCancelAdd {α : Type u_1} [Add α] [h : IsRightCancelAdd α] :

IsRightCancelAdd αᵒᵈ

instance OrderDual.instIsCancelMul {α : Type u_1} [Mul α] [h : IsCancelMul α] :

IsCancelMul αᵒᵈ

instance OrderDual.instIsCancelAdd {α : Type u_1} [Add α] [h : IsCancelAdd α] :

IsCancelAdd αᵒᵈ

@[implicit_reducible]

instance OrderDual.instLeftCancelSemigroup {α : Type u_1} [h : LeftCancelSemigroup α] :

LeftCancelSemigroup αᵒᵈ

AddLeftCancelSemigroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddLeftCancelSemigroup {α : Type u_1} [h : AddLeftCancelSemigroup α] :

@[implicit_reducible]

instance OrderDual.instRightCancelSemigroup {α : Type u_1} [h : RightCancelSemigroup α] :

RightCancelSemigroup αᵒᵈ

AddRightCancelSemigroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddRightCancelSemigroup {α : Type u_1} [h : AddRightCancelSemigroup α] :

@[implicit_reducible]

instance OrderDual.instMulOneClass {α : Type u_1} [h : MulOneClass α] :

MulOneClass αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddZeroClass {α : Type u_1} [h : AddZeroClass α] :

AddZeroClass αᵒᵈ

@[implicit_reducible]

instance OrderDual.instMonoid {α : Type u_1} [h : Monoid α] :

Monoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddMonoid {α : Type u_1} [h : AddMonoid α] :

AddMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommMonoid {α : Type u_1} [h : CommMonoid α] :

CommMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCommMonoid {α : Type u_1} [h : AddCommMonoid α] :

AddCommMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instLeftCancelMonoid {α : Type u_1} [h : LeftCancelMonoid α] :

LeftCancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddLeftCancelMonoid {α : Type u_1} [h : AddLeftCancelMonoid α] :

AddLeftCancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instRightCancelMonoid {α : Type u_1} [h : RightCancelMonoid α] :

RightCancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddRightCancelMonoid {α : Type u_1} [h : AddRightCancelMonoid α] :

AddRightCancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCancelMonoid {α : Type u_1} [h : CancelMonoid α] :

CancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCancelMonoid {α : Type u_1} [h : AddCancelMonoid α] :

AddCancelMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCancelCommMonoid {α : Type u_1} [h : CancelCommMonoid α] :

CancelCommMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCancelCommMonoid {α : Type u_1} [h : AddCancelCommMonoid α] :

AddCancelCommMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instInvolutiveInv {α : Type u_1} [h : InvolutiveInv α] :

InvolutiveInv αᵒᵈ

@[implicit_reducible]

instance OrderDual.instInvolutiveNeg {α : Type u_1} [h : InvolutiveNeg α] :

InvolutiveNeg αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDivInvMonoid {α : Type u_1} [h : DivInvMonoid α] :

DivInvMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instSubNegAddMonoid {α : Type u_1} [h : SubNegMonoid α] :

SubNegMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDivisionMonoid {α : Type u_1} [h : DivisionMonoid α] :

DivisionMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instSubtractionMonoid {α : Type u_1} [h : SubtractionMonoid α] :

SubtractionMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDivisionCommMonoid {α : Type u_1} [h : DivisionCommMonoid α] :

DivisionCommMonoid αᵒᵈ

SubtractionCommMonoid αᵒᵈ

@[implicit_reducible]

instance OrderDual.instDivisionAddCommMonoid {α : Type u_1} [h : SubtractionCommMonoid α] :

@[implicit_reducible]

instance OrderDual.instGroup {α : Type u_1} [h : Group α] :

Group αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddGroup {α : Type u_1} [h : AddGroup α] :

AddGroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instCommGroup {α : Type u_1} [h : CommGroup α] :

CommGroup αᵒᵈ

@[implicit_reducible]

instance OrderDual.instAddCommGroup {α : Type u_1} [h : AddCommGroup α] :

AddCommGroup αᵒᵈ

@[simp]

theorem toDual_one {α : Type u_1} [One α] :

OrderDual.toDual 1 = 1

@[simp]

theorem toDual_zero {α : Type u_1} [Zero α] :

OrderDual.toDual 0 = 0

@[simp]

theorem ofDual_one {α : Type u_1} [One α] :

OrderDual.ofDual 1 = 1

@[simp]

theorem ofDual_zero {α : Type u_1} [Zero α] :

OrderDual.ofDual 0 = 0

@[simp]

theorem toDual_eq_one {α : Type u_1} [One α] {a : α} :

OrderDual.toDual a = 1 ↔ a = 1

@[simp]

theorem toDual_eq_zero {α : Type u_1} [Zero α] {a : α} :

OrderDual.toDual a = 0 ↔ a = 0

@[simp]

theorem ofDual_eq_one {α : Type u_1} [One α] {a : αᵒᵈ} :

OrderDual.ofDual a = 1 ↔ a = 1

@[simp]

theorem ofDual_eq_zero {α : Type u_1} [Zero α] {a : αᵒᵈ} :

OrderDual.ofDual a = 0 ↔ a = 0

@[simp]

theorem toDual_mul {α : Type u_1} [Mul α] (a b : α) :

OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b

@[simp]

theorem toDual_add {α : Type u_1} [Add α] (a b : α) :

OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b

@[simp]

theorem ofDual_mul {α : Type u_1} [Mul α] (a b : αᵒᵈ) :

OrderDual.ofDual (a * b) = OrderDual.ofDual a * OrderDual.ofDual b

@[simp]

theorem ofDual_add {α : Type u_1} [Add α] (a b : αᵒᵈ) :

OrderDual.ofDual (a + b) = OrderDual.ofDual a + OrderDual.ofDual b

@[simp]

theorem toDual_inv {α : Type u_1} [Inv α] (a : α) :

OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹

@[simp]

theorem toDual_neg {α : Type u_1} [Neg α] (a : α) :

OrderDual.toDual (-a) = -OrderDual.toDual a

@[simp]

theorem ofDual_inv {α : Type u_1} [Inv α] (a : αᵒᵈ) :

OrderDual.ofDual a⁻¹ = (OrderDual.ofDual a)⁻¹

@[simp]

theorem ofDual_neg {α : Type u_1} [Neg α] (a : αᵒᵈ) :

OrderDual.ofDual (-a) = -OrderDual.ofDual a

@[simp]

theorem toDual_div {α : Type u_1} [Div α] (a b : α) :

OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b

@[simp]

theorem toDual_sub {α : Type u_1} [Sub α] (a b : α) :

OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b

@[simp]

theorem ofDual_div {α : Type u_1} [Div α] (a b : αᵒᵈ) :

OrderDual.ofDual (a / b) = OrderDual.ofDual a / OrderDual.ofDual b

@[simp]

theorem ofDual_sub {α : Type u_1} [Sub α] (a b : αᵒᵈ) :

OrderDual.ofDual (a - b) = OrderDual.ofDual a - OrderDual.ofDual b

@[simp]

theorem toDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b

@[simp]

theorem toDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

OrderDual.toDual (b • a) = b • OrderDual.toDual a

@[simp]

theorem toDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a

@[simp]

theorem ofDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵒᵈ) (b : β) :

OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b

@[simp]

theorem ofDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : αᵒᵈ) :

OrderDual.ofDual (b • a) = b • OrderDual.ofDual a

@[simp]

theorem ofDual_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : αᵒᵈ) :

OrderDual.ofDual (b +ᵥ a) = b +ᵥ OrderDual.ofDual a

@[simp]

theorem pow_toDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

a ^ OrderDual.toDual b = a ^ b

@[simp]

theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

OrderDual.toDual b +ᵥ a = b +ᵥ a

@[simp]

theorem toDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

OrderDual.toDual b • a = b • a

@[simp]

theorem pow_ofDual {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : βᵒᵈ) :

a ^ OrderDual.ofDual b = a ^ b

@[simp]

theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : βᵒᵈ) (a : α) :

OrderDual.ofDual b • a = b • a

@[simp]

theorem ofDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : βᵒᵈ) (a : α) :

OrderDual.ofDual b +ᵥ a = b +ᵥ a

@[simp]

theorem isLeftRegular_toDual {α : Type u_1} [Monoid α] {a : α} :

IsLeftRegular (OrderDual.toDual a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :

IsAddLeftRegular (OrderDual.toDual a) ↔ IsAddLeftRegular a

@[simp]

theorem isLeftRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :

IsLeftRegular (OrderDual.ofDual a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :

IsAddLeftRegular (OrderDual.ofDual a) ↔ IsAddLeftRegular a

@[simp]

theorem isRightRegular_toDual {α : Type u_1} [Monoid α] {a : α} :

IsRightRegular (OrderDual.toDual a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRightRegular (OrderDual.toDual a) ↔ IsAddRightRegular a

@[simp]

theorem isRightRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :

IsRightRegular (OrderDual.ofDual a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :

IsAddRightRegular (OrderDual.ofDual a) ↔ IsAddRightRegular a

@[simp]

theorem isRegular_toDual {α : Type u_1} [Monoid α] {a : α} :

IsRegular (OrderDual.toDual a) ↔ IsRegular a

@[simp]

theorem isAddRegular_toDual {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRegular (OrderDual.toDual a) ↔ IsAddRegular a

@[simp]

theorem isRegular_ofDual {α : Type u_1} [Monoid α] {a : αᵒᵈ} :

IsRegular (OrderDual.ofDual a) ↔ IsRegular a

@[simp]

theorem isAddRegular_ofDual {α : Type u_1} [AddMonoid α] {a : αᵒᵈ} :

IsAddRegular (OrderDual.ofDual a) ↔ IsAddRegular a

Lexicographical order #

@[implicit_reducible]

instance instOneLex {α : Type u_1} [h : One α] :

One (Lex α)

@[implicit_reducible]

instance instZeroLex {α : Type u_1} [h : Zero α] :

Zero (Lex α)

@[implicit_reducible]

instance instMulLex {α : Type u_1} [h : Mul α] :

Mul (Lex α)

@[implicit_reducible]

instance instAddLex {α : Type u_1} [h : Add α] :

Add (Lex α)

@[implicit_reducible]

instance instInvLex {α : Type u_1} [h : Inv α] :

Inv (Lex α)

@[implicit_reducible]

instance instNegLex {α : Type u_1} [h : Neg α] :

Neg (Lex α)

@[implicit_reducible]

instance instDivLex {α : Type u_1} [h : Div α] :

Div (Lex α)

@[implicit_reducible]

instance instSubLex {α : Type u_1} [h : Sub α] :

Sub (Lex α)

@[implicit_reducible]

instance Lex.instPow {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow (Lex α) β

@[implicit_reducible]

instance Lex.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd β (Lex α)

@[implicit_reducible]

instance Lex.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul β (Lex α)

@[implicit_reducible]

instance Lex.instPow' {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow α (Lex β)

@[implicit_reducible]

instance Lex.instVAdd' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd (Lex β) α

@[implicit_reducible]

instance Lex.instSMul' {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul (Lex β) α

@[implicit_reducible]

instance instSemigroupLex {α : Type u_1} [h : Semigroup α] :

Semigroup (Lex α)

@[implicit_reducible]

instance instAddSemigroupLex {α : Type u_1} [h : AddSemigroup α] :

AddSemigroup (Lex α)

@[implicit_reducible]

instance instCommSemigroupLex {α : Type u_1} [h : CommSemigroup α] :

CommSemigroup (Lex α)

@[implicit_reducible]

instance instAddCommSemigroupLex {α : Type u_1} [h : AddCommSemigroup α] :

AddCommSemigroup (Lex α)

instance instIsLeftCancelMulLex {α : Type u_1} [Mul α] [IsLeftCancelMul α] :

IsLeftCancelMul (Lex α)

instance instIsLeftCancelAddLex {α : Type u_1} [Add α] [IsLeftCancelAdd α] :

IsLeftCancelAdd (Lex α)

instance instIsRightCancelMulLex {α : Type u_1} [Mul α] [IsRightCancelMul α] :

IsRightCancelMul (Lex α)

instance instIsRightCancelAddLex {α : Type u_1} [Add α] [IsRightCancelAdd α] :

IsRightCancelAdd (Lex α)

instance instIsCancelMulLex {α : Type u_1} [Mul α] [IsCancelMul α] :

IsCancelMul (Lex α)

instance instIsCancelAddLex {α : Type u_1} [Add α] [IsCancelAdd α] :

IsCancelAdd (Lex α)

@[implicit_reducible]

instance instLeftCancelSemigroupLex {α : Type u_1} [h : LeftCancelSemigroup α] :

LeftCancelSemigroup (Lex α)

@[implicit_reducible]

instance instAddLeftCancelSemigroupLex {α : Type u_1} [h : AddLeftCancelSemigroup α] :

AddLeftCancelSemigroup (Lex α)

@[implicit_reducible]

instance instRightCancelSemigroupLex {α : Type u_1} [h : RightCancelSemigroup α] :

RightCancelSemigroup (Lex α)

@[implicit_reducible]

instance instAddRightCancelSemigroupLex {α : Type u_1} [h : AddRightCancelSemigroup α] :

AddRightCancelSemigroup (Lex α)

@[implicit_reducible]

instance instMulOneClassLex {α : Type u_1} [h : MulOneClass α] :

MulOneClass (Lex α)

@[implicit_reducible]

instance instAddZeroClassLex {α : Type u_1} [h : AddZeroClass α] :

AddZeroClass (Lex α)

@[implicit_reducible]

instance instMonoidLex {α : Type u_1} [h : Monoid α] :

Monoid (Lex α)

@[implicit_reducible]

instance instAddMonoidLex {α : Type u_1} [h : AddMonoid α] :

AddMonoid (Lex α)

@[implicit_reducible]

instance instCommMonoidLex {α : Type u_1} [h : CommMonoid α] :

CommMonoid (Lex α)

@[implicit_reducible]

instance instAddCommMonoidLex {α : Type u_1} [h : AddCommMonoid α] :

AddCommMonoid (Lex α)

@[implicit_reducible]

instance instLeftCancelMonoidLex {α : Type u_1} [h : LeftCancelMonoid α] :

LeftCancelMonoid (Lex α)

@[implicit_reducible]

instance instAddLeftCancelMonoidLex {α : Type u_1} [h : AddLeftCancelMonoid α] :

AddLeftCancelMonoid (Lex α)

@[implicit_reducible]

instance instRightCancelMonoidLex {α : Type u_1} [h : RightCancelMonoid α] :

RightCancelMonoid (Lex α)

@[implicit_reducible]

instance instAddRightCancelMonoidLex {α : Type u_1} [h : AddRightCancelMonoid α] :

AddRightCancelMonoid (Lex α)

@[implicit_reducible]

instance instCancelMonoidLex {α : Type u_1} [h : CancelMonoid α] :

CancelMonoid (Lex α)

@[implicit_reducible]

instance instAddCancelMonoidLex {α : Type u_1} [h : AddCancelMonoid α] :

AddCancelMonoid (Lex α)

@[implicit_reducible]

instance instCancelCommMonoidLex {α : Type u_1} [h : CancelCommMonoid α] :

CancelCommMonoid (Lex α)

@[implicit_reducible]

instance instAddCancelCommMonoidLex {α : Type u_1} [h : AddCancelCommMonoid α] :

AddCancelCommMonoid (Lex α)

@[implicit_reducible]

instance instInvolutiveInvLex {α : Type u_1} [h : InvolutiveInv α] :

InvolutiveInv (Lex α)

@[implicit_reducible]

instance instInvolutiveNegLex {α : Type u_1} [h : InvolutiveNeg α] :

InvolutiveNeg (Lex α)

@[implicit_reducible]

instance instDivInvMonoidLex {α : Type u_1} [h : DivInvMonoid α] :

DivInvMonoid (Lex α)

@[implicit_reducible]

instance instSubNegAddMonoidLex {α : Type u_1} [h : SubNegMonoid α] :

SubNegMonoid (Lex α)

@[implicit_reducible]

instance instDivisionMonoidLex {α : Type u_1} [h : DivisionMonoid α] :

DivisionMonoid (Lex α)

@[implicit_reducible]

instance instSubtractionMonoidLex {α : Type u_1} [h : SubtractionMonoid α] :

SubtractionMonoid (Lex α)

@[implicit_reducible]

instance instDivisionCommMonoidLex {α : Type u_1} [h : DivisionCommMonoid α] :

DivisionCommMonoid (Lex α)

@[implicit_reducible]

instance instDivisionAddCommMonoidLex {α : Type u_1} [h : SubtractionCommMonoid α] :

SubtractionCommMonoid (Lex α)

@[implicit_reducible]

instance instGroupLex {α : Type u_1} [h : Group α] :

Group (Lex α)

@[implicit_reducible]

instance instAddGroupLex {α : Type u_1} [h : AddGroup α] :

AddGroup (Lex α)

@[implicit_reducible]

instance instCommGroupLex {α : Type u_1} [h : CommGroup α] :

CommGroup (Lex α)

@[implicit_reducible]

instance instAddCommGroupLex {α : Type u_1} [h : AddCommGroup α] :

AddCommGroup (Lex α)

@[simp]

theorem toLex_one {α : Type u_1} [One α] :

toLex 1 = 1

@[simp]

theorem toLex_zero {α : Type u_1} [Zero α] :

toLex 0 = 0

@[simp]

theorem toLex_eq_one {α : Type u_1} [One α] {a : α} :

toLex a = 1 ↔ a = 1

@[simp]

theorem toLex_eq_zero {α : Type u_1} [Zero α] {a : α} :

toLex a = 0 ↔ a = 0

@[simp]

theorem ofLex_one {α : Type u_1} [One α] :

ofLex 1 = 1

@[simp]

theorem ofLex_zero {α : Type u_1} [Zero α] :

ofLex 0 = 0

@[simp]

theorem ofLex_eq_one {α : Type u_1} [One α] {a : Lex α} :

ofLex a = 1 ↔ a = 1

@[simp]

theorem ofLex_eq_zero {α : Type u_1} [Zero α] {a : Lex α} :

ofLex a = 0 ↔ a = 0

@[simp]

theorem toLex_mul {α : Type u_1} [Mul α] (a b : α) :

toLex (a * b) = toLex a * toLex b

@[simp]

theorem toLex_add {α : Type u_1} [Add α] (a b : α) :

toLex (a + b) = toLex a + toLex b

@[simp]

theorem ofLex_mul {α : Type u_1} [Mul α] (a b : Lex α) :

ofLex (a * b) = ofLex a * ofLex b

@[simp]

theorem ofLex_add {α : Type u_1} [Add α] (a b : Lex α) :

ofLex (a + b) = ofLex a + ofLex b

@[simp]

theorem toLex_inv {α : Type u_1} [Inv α] (a : α) :

toLex a⁻¹ = (toLex a)⁻¹

@[simp]

theorem toLex_neg {α : Type u_1} [Neg α] (a : α) :

toLex (-a) = -toLex a

@[simp]

theorem ofLex_inv {α : Type u_1} [Inv α] (a : Lex α) :

ofLex a⁻¹ = (ofLex a)⁻¹

@[simp]

theorem ofLex_neg {α : Type u_1} [Neg α] (a : Lex α) :

ofLex (-a) = -ofLex a

@[simp]

theorem toLex_div {α : Type u_1} [Div α] (a b : α) :

toLex (a / b) = toLex a / toLex b

@[simp]

theorem toLex_sub {α : Type u_1} [Sub α] (a b : α) :

toLex (a - b) = toLex a - toLex b

@[simp]

theorem ofLex_div {α : Type u_1} [Div α] (a b : Lex α) :

ofLex (a / b) = ofLex a / ofLex b

@[simp]

theorem ofLex_sub {α : Type u_1} [Sub α] (a b : Lex α) :

ofLex (a - b) = ofLex a - ofLex b

@[simp]

theorem toLex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

toLex (a ^ b) = toLex a ^ b

@[simp]

theorem toLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toLex (b +ᵥ a) = b +ᵥ toLex a

@[simp]

theorem toLex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toLex (b • a) = b • toLex a

@[simp]

theorem ofLex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : Lex α) (b : β) :

ofLex (a ^ b) = ofLex a ^ b

@[simp]

theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Lex α) :

ofLex (b +ᵥ a) = b +ᵥ ofLex a

@[simp]

theorem ofLex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : Lex α) :

ofLex (b • a) = b • ofLex a

@[simp]

theorem pow_toLex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

a ^ toLex b = a ^ b

@[simp]

theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toLex b +ᵥ a = b +ᵥ a

@[simp]

theorem toLex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toLex b • a = b • a

@[simp]

theorem pow_ofLex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : Lex β) :

a ^ ofLex b = a ^ b

@[simp]

theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : Lex β) (a : α) :

ofLex b +ᵥ a = b +ᵥ a

@[simp]

theorem ofLex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Lex β) (a : α) :

ofLex b • a = b • a

@[simp]

theorem isLeftRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsLeftRegular (toLex a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddLeftRegular (toLex a) ↔ IsAddLeftRegular a

@[simp]

theorem isLeftRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsLeftRegular (ofLex a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddLeftRegular (ofLex a) ↔ IsAddLeftRegular a

@[simp]

theorem isRightRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsRightRegular (toLex a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRightRegular (toLex a) ↔ IsAddRightRegular a

@[simp]

theorem isRightRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsRightRegular (ofLex a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddRightRegular (ofLex a) ↔ IsAddRightRegular a

@[simp]

theorem isRegular_toLex {α : Type u_1} [Monoid α] {a : α} :

IsRegular (toLex a) ↔ IsRegular a

@[simp]

theorem isAddRegular_toLex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRegular (toLex a) ↔ IsAddRegular a

@[simp]

theorem isRegular_ofLex {α : Type u_1} [Monoid α] {a : Lex α} :

IsRegular (ofLex a) ↔ IsRegular a

@[simp]

theorem isAddRegular_ofLex {α : Type u_1} [AddMonoid α] {a : Lex α} :

IsAddRegular (ofLex a) ↔ IsAddRegular a

Colexicographical order #

@[implicit_reducible]

instance instOneColex {α : Type u_1} [h : One α] :

One (Colex α)

@[implicit_reducible]

instance instZeroColex {α : Type u_1} [h : Zero α] :

Zero (Colex α)

@[implicit_reducible]

instance instMulColex {α : Type u_1} [h : Mul α] :

Mul (Colex α)

@[implicit_reducible]

instance instAddColex {α : Type u_1} [h : Add α] :

Add (Colex α)

@[implicit_reducible]

instance instInvColex {α : Type u_1} [h : Inv α] :

Inv (Colex α)

@[implicit_reducible]

instance instNegColex {α : Type u_1} [h : Neg α] :

Neg (Colex α)

@[implicit_reducible]

instance instDivColex {α : Type u_1} [h : Div α] :

Div (Colex α)

@[implicit_reducible]

instance instSubColex {α : Type u_1} [h : Sub α] :

Sub (Colex α)

@[implicit_reducible]

instance Colex.instPow {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow (Colex α) β

@[implicit_reducible]

instance Colex.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul β (Colex α)

@[implicit_reducible]

instance Colex.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd β (Colex α)

@[implicit_reducible]

instance Colex.instPow' {α : Type u_1} {β : Type u_2} [h : Pow α β] :

Pow α (Colex β)

@[implicit_reducible]

instance Colex.instVAdd' {β : Type u_2} {α : Type u_1} [h : VAdd β α] :

VAdd (Colex β) α

@[implicit_reducible]

instance Colex.instSMul' {β : Type u_2} {α : Type u_1} [h : SMul β α] :

SMul (Colex β) α

@[implicit_reducible]

instance instSemigroupColex {α : Type u_1} [h : Semigroup α] :

Semigroup (Colex α)

@[implicit_reducible]

instance instAddSemigroupColex {α : Type u_1} [h : AddSemigroup α] :

AddSemigroup (Colex α)

@[implicit_reducible]

instance instCommSemigroupColex {α : Type u_1} [h : CommSemigroup α] :

CommSemigroup (Colex α)

@[implicit_reducible]

instance instAddCommSemigroupColex {α : Type u_1} [h : AddCommSemigroup α] :

AddCommSemigroup (Colex α)

instance instIsLeftCancelMulColex {α : Type u_1} [Mul α] [IsLeftCancelMul α] :

IsLeftCancelMul (Colex α)

instance instIsLeftCancelAddColex {α : Type u_1} [Add α] [IsLeftCancelAdd α] :

IsLeftCancelAdd (Colex α)

instance instIsRightCancelMulColex {α : Type u_1} [Mul α] [IsRightCancelMul α] :

IsRightCancelMul (Colex α)

instance instIsRightCancelAddColex {α : Type u_1} [Add α] [IsRightCancelAdd α] :

IsRightCancelAdd (Colex α)

instance instIsCancelMulColex {α : Type u_1} [Mul α] [IsCancelMul α] :

IsCancelMul (Colex α)

instance instIsCancelAddColex {α : Type u_1} [Add α] [IsCancelAdd α] :

IsCancelAdd (Colex α)

@[implicit_reducible]

instance instLeftCancelSemigroupColex {α : Type u_1} [h : LeftCancelSemigroup α] :

LeftCancelSemigroup (Colex α)

@[implicit_reducible]

instance instAddLeftCancelSemigroupColex {α : Type u_1} [h : AddLeftCancelSemigroup α] :

AddLeftCancelSemigroup (Colex α)

@[implicit_reducible]

instance instRightCancelSemigroupColex {α : Type u_1} [h : RightCancelSemigroup α] :

RightCancelSemigroup (Colex α)

@[implicit_reducible]

instance instAddRightCancelSemigroupColex {α : Type u_1} [h : AddRightCancelSemigroup α] :

AddRightCancelSemigroup (Colex α)

@[implicit_reducible]

instance instMulOneClassColex {α : Type u_1} [h : MulOneClass α] :

MulOneClass (Colex α)

@[implicit_reducible]

instance instAddZeroClassColex {α : Type u_1} [h : AddZeroClass α] :

AddZeroClass (Colex α)

@[implicit_reducible]

instance instMonoidColex {α : Type u_1} [h : Monoid α] :

Monoid (Colex α)

@[implicit_reducible]

instance instAddMonoidColex {α : Type u_1} [h : AddMonoid α] :

AddMonoid (Colex α)

@[implicit_reducible]

instance instCommMonoidColex {α : Type u_1} [h : CommMonoid α] :

CommMonoid (Colex α)

@[implicit_reducible]

instance instAddCommMonoidColex {α : Type u_1} [h : AddCommMonoid α] :

AddCommMonoid (Colex α)

@[implicit_reducible]

instance instLeftCancelMonoidColex {α : Type u_1} [h : LeftCancelMonoid α] :

LeftCancelMonoid (Colex α)

@[implicit_reducible]

instance instAddLeftCancelMonoidColex {α : Type u_1} [h : AddLeftCancelMonoid α] :

AddLeftCancelMonoid (Colex α)

@[implicit_reducible]

instance instRightCancelMonoidColex {α : Type u_1} [h : RightCancelMonoid α] :

RightCancelMonoid (Colex α)

@[implicit_reducible]

instance instAddRightCancelMonoidColex {α : Type u_1} [h : AddRightCancelMonoid α] :

AddRightCancelMonoid (Colex α)

@[implicit_reducible]

instance instCancelMonoidColex {α : Type u_1} [h : CancelMonoid α] :

CancelMonoid (Colex α)

@[implicit_reducible]

instance instAddCancelMonoidColex {α : Type u_1} [h : AddCancelMonoid α] :

AddCancelMonoid (Colex α)

@[implicit_reducible]

instance instCancelCommMonoidColex {α : Type u_1} [h : CancelCommMonoid α] :

CancelCommMonoid (Colex α)

@[implicit_reducible]

instance instAddCancelCommMonoidColex {α : Type u_1} [h : AddCancelCommMonoid α] :

AddCancelCommMonoid (Colex α)

@[implicit_reducible]

instance instInvolutiveInvColex {α : Type u_1} [h : InvolutiveInv α] :

InvolutiveInv (Colex α)

@[implicit_reducible]

instance instInvolutiveNegColex {α : Type u_1} [h : InvolutiveNeg α] :

InvolutiveNeg (Colex α)

@[implicit_reducible]

instance instDivInvMonoidColex {α : Type u_1} [h : DivInvMonoid α] :

DivInvMonoid (Colex α)

@[implicit_reducible]

instance instSubNegAddMonoidColex {α : Type u_1} [h : SubNegMonoid α] :

SubNegMonoid (Colex α)

@[implicit_reducible]

instance instDivisionMonoidColex {α : Type u_1} [h : DivisionMonoid α] :

DivisionMonoid (Colex α)

@[implicit_reducible]

instance instSubtractionMonoidColex {α : Type u_1} [h : SubtractionMonoid α] :

SubtractionMonoid (Colex α)

@[implicit_reducible]

instance instDivisionCommMonoidColex {α : Type u_1} [h : DivisionCommMonoid α] :

DivisionCommMonoid (Colex α)

@[implicit_reducible]

instance instDivisionAddCommMonoidColex {α : Type u_1} [h : SubtractionCommMonoid α] :

SubtractionCommMonoid (Colex α)

@[implicit_reducible]

instance instGroupColex {α : Type u_1} [h : Group α] :

Group (Colex α)

@[implicit_reducible]

instance instAddGroupColex {α : Type u_1} [h : AddGroup α] :

AddGroup (Colex α)

@[implicit_reducible]

instance instCommGroupColex {α : Type u_1} [h : CommGroup α] :

CommGroup (Colex α)

@[implicit_reducible]

instance instAddCommGroupColex {α : Type u_1} [h : AddCommGroup α] :

AddCommGroup (Colex α)

@[simp]

theorem toColex_one {α : Type u_1} [One α] :

toColex 1 = 1

@[simp]

theorem toColex_zero {α : Type u_1} [Zero α] :

toColex 0 = 0

@[simp]

theorem toColex_eq_one {α : Type u_1} [One α] {a : α} :

toColex a = 1 ↔ a = 1

@[simp]

theorem toColex_eq_zero {α : Type u_1} [Zero α] {a : α} :

toColex a = 0 ↔ a = 0

@[simp]

theorem ofColex_one {α : Type u_1} [One α] :

ofColex 1 = 1

@[simp]

theorem ofColex_zero {α : Type u_1} [Zero α] :

ofColex 0 = 0

@[simp]

theorem ofColex_eq_one {α : Type u_1} [One α] {a : Colex α} :

ofColex a = 1 ↔ a = 1

@[simp]

theorem ofColex_eq_zero {α : Type u_1} [Zero α] {a : Colex α} :

ofColex a = 0 ↔ a = 0

@[simp]

theorem toColex_mul {α : Type u_1} [Mul α] (a b : α) :

toColex (a * b) = toColex a * toColex b

@[simp]

theorem toColex_add {α : Type u_1} [Add α] (a b : α) :

toColex (a + b) = toColex a + toColex b

@[simp]

theorem ofColex_mul {α : Type u_1} [Mul α] (a b : Colex α) :

ofColex (a * b) = ofColex a * ofColex b

@[simp]

theorem ofColex_add {α : Type u_1} [Add α] (a b : Colex α) :

ofColex (a + b) = ofColex a + ofColex b

@[simp]

theorem toColex_inv {α : Type u_1} [Inv α] (a : α) :

toColex a⁻¹ = (toColex a)⁻¹

@[simp]

theorem toColex_neg {α : Type u_1} [Neg α] (a : α) :

toColex (-a) = -toColex a

@[simp]

theorem ofColex_inv {α : Type u_1} [Inv α] (a : Colex α) :

ofColex a⁻¹ = (ofColex a)⁻¹

@[simp]

theorem ofColex_neg {α : Type u_1} [Neg α] (a : Colex α) :

ofColex (-a) = -ofColex a

@[simp]

theorem toColex_div {α : Type u_1} [Div α] (a b : α) :

toColex (a / b) = toColex a / toColex b

@[simp]

theorem toColex_sub {α : Type u_1} [Sub α] (a b : α) :

toColex (a - b) = toColex a - toColex b

@[simp]

theorem ofColex_div {α : Type u_1} [Div α] (a b : Colex α) :

ofColex (a / b) = ofColex a / ofColex b

@[simp]

theorem ofColex_sub {α : Type u_1} [Sub α] (a b : Colex α) :

ofColex (a - b) = ofColex a - ofColex b

@[simp]

theorem toColex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

toColex (a ^ b) = toColex a ^ b

@[simp]

theorem toColex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toColex (b • a) = b • toColex a

@[simp]

theorem toColex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toColex (b +ᵥ a) = b +ᵥ toColex a

@[simp]

theorem ofColex_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : Colex α) (b : β) :

ofColex (a ^ b) = ofColex a ^ b

@[simp]

theorem ofColex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : Colex α) :

ofColex (b • a) = b • ofColex a

@[simp]

theorem ofColex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Colex α) :

ofColex (b +ᵥ a) = b +ᵥ ofColex a

@[simp]

theorem pow_toColex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :

a ^ toColex b = a ^ b

@[simp]

theorem toColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :

toColex b +ᵥ a = b +ᵥ a

@[simp]

theorem toColex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :

toColex b • a = b • a

@[simp]

theorem pow_ofColex {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : Colex β) :

a ^ ofColex b = a ^ b

@[simp]

theorem ofColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : Colex β) (a : α) :

ofColex b +ᵥ a = b +ᵥ a

@[simp]

theorem ofColex_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Colex β) (a : α) :

ofColex b • a = b • a

@[simp]

theorem isLeftRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsLeftRegular (toColex a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddLeftRegular (toColex a) ↔ IsAddLeftRegular a

@[simp]

theorem isLeftRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsLeftRegular (ofColex a) ↔ IsLeftRegular a

@[simp]

theorem isAddLeftRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} :

IsAddLeftRegular (ofColex a) ↔ IsAddLeftRegular a

@[simp]

theorem isRightRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsRightRegular (toColex a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRightRegular (toColex a) ↔ IsAddRightRegular a

@[simp]

theorem isRightRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsRightRegular (ofColex a) ↔ IsRightRegular a

@[simp]

theorem isAddRightRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} :

IsAddRightRegular (ofColex a) ↔ IsAddRightRegular a

@[simp]

theorem isRegular_toColex {α : Type u_1} [Monoid α] {a : α} :

IsRegular (toColex a) ↔ IsRegular a

@[simp]

theorem isAddRegular_toColex {α : Type u_1} [AddMonoid α] {a : α} :

IsAddRegular (toColex a) ↔ IsAddRegular a

@[simp]

theorem isRegular_ofColex {α : Type u_1} [Monoid α] {a : Colex α} :

IsRegular (ofColex a) ↔ IsRegular a