Group structure on the order type synonyms #

Transfer algebraic instances from α to αᵒᵈ, Lex α, and Colex α.

`OrderDual` #

source

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

One αᵒᵈ

Equations

source

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

Zero αᵒᵈ

Equations

source

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

Mul αᵒᵈ

Equations

source

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

Add αᵒᵈ

Equations

source

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

Inv αᵒᵈ

Equations

source

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

Neg αᵒᵈ

Equations

source

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

Div αᵒᵈ

Equations

source

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

Sub αᵒᵈ

Equations

source

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

Pow αᵒᵈ β

Equations

source

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

SMul β αᵒᵈ

Equations

source

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

VAdd β αᵒᵈ

Equations

source

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

Pow α βᵒᵈ

Equations

source

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

VAdd βᵒᵈ α

Equations

source

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

SMul βᵒᵈ α

Equations

source

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

Semigroup αᵒᵈ

Equations

source

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

AddSemigroup αᵒᵈ

Equations

source

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

CommSemigroup αᵒᵈ

Equations

source

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

AddCommSemigroup αᵒᵈ

Equations

source

instance instIsLeftCancelMulOrderDual {α : Type u_1} [Mul α] [h : IsLeftCancelMul α] :

IsLeftCancelMul αᵒᵈ

source

instance instIsLeftCancelAddOrderDual {α : Type u_1} [Add α] [h : IsLeftCancelAdd α] :

IsLeftCancelAdd αᵒᵈ

source

instance instIsRightCancelMulOrderDual {α : Type u_1} [Mul α] [h : IsRightCancelMul α] :

IsRightCancelMul αᵒᵈ

source

instance instIsRightCancelAddOrderDual {α : Type u_1} [Add α] [h : IsRightCancelAdd α] :

IsRightCancelAdd αᵒᵈ

source

instance instIsCancelMulOrderDual {α : Type u_1} [Mul α] [h : IsCancelMul α] :

IsCancelMul αᵒᵈ

source

instance instIsCancelAddOrderDual {α : Type u_1} [Add α] [h : IsCancelAdd α] :

IsCancelAdd αᵒᵈ

source

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

LeftCancelSemigroup αᵒᵈ

Equations

source

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

AddLeftCancelSemigroup αᵒᵈ

Equations

source

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

RightCancelSemigroup αᵒᵈ

Equations

source

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

AddRightCancelSemigroup αᵒᵈ

Equations

source

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

MulOneClass αᵒᵈ

Equations

source

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

AddZeroClass αᵒᵈ

Equations

source

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

Monoid αᵒᵈ

Equations

source

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

AddMonoid αᵒᵈ

Equations

source

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

CommMonoid αᵒᵈ

Equations

source

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

AddCommMonoid αᵒᵈ

Equations

source

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

LeftCancelMonoid αᵒᵈ

Equations

source

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

AddLeftCancelMonoid αᵒᵈ

Equations

source

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

RightCancelMonoid αᵒᵈ

Equations

source

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

AddRightCancelMonoid αᵒᵈ

Equations

source

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

CancelMonoid αᵒᵈ

Equations

source

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

AddCancelMonoid αᵒᵈ

Equations

source

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

CancelCommMonoid αᵒᵈ

Equations

source

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

AddCancelCommMonoid αᵒᵈ

Equations

source

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

InvolutiveInv αᵒᵈ

Equations

source

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

InvolutiveNeg αᵒᵈ

Equations

source

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

DivInvMonoid αᵒᵈ

Equations

source

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

SubNegMonoid αᵒᵈ

Equations

source

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

DivisionMonoid αᵒᵈ

Equations

source

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

SubtractionMonoid αᵒᵈ

Equations

source

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

DivisionCommMonoid αᵒᵈ

Equations

source

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

SubtractionCommMonoid αᵒᵈ

Equations

source

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

Group αᵒᵈ

Equations

source

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

AddGroup αᵒᵈ

Equations

source

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

CommGroup αᵒᵈ

Equations

source

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

AddCommGroup αᵒᵈ

Equations

source

@[simp]

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

OrderDual.toDual 1 = 1

source

@[simp]

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

OrderDual.toDual 0 = 0

source

@[simp]

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

OrderDual.ofDual 1 = 1

source

@[simp]

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

OrderDual.ofDual 0 = 0

source

@[simp]

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

OrderDual.toDual a = 1 ↔ a = 1

source

@[simp]

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

OrderDual.toDual a = 0 ↔ a = 0

source

@[simp]

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

OrderDual.ofDual a = 1 ↔ a = 1

source

@[simp]

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

OrderDual.ofDual a = 0 ↔ a = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

a ^ OrderDual.toDual b = a ^ b

source

@[simp]

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

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

source

@[simp]

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

OrderDual.toDual b • a = b • a

source

@[simp]

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

a ^ OrderDual.ofDual b = a ^ b

source

@[simp]

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

OrderDual.ofDual b • a = b • a

source

@[simp]

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

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

source

@[simp]

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

IsLeftRegular (OrderDual.toDual a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (OrderDual.toDual a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsLeftRegular (OrderDual.ofDual a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (OrderDual.ofDual a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsRightRegular (OrderDual.toDual a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (OrderDual.toDual a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRightRegular (OrderDual.ofDual a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (OrderDual.ofDual a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRegular (OrderDual.toDual a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (OrderDual.toDual a) ↔ IsAddRegular a

source

@[simp]

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

IsRegular (OrderDual.ofDual a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (OrderDual.ofDual a) ↔ IsAddRegular a

Lexicographical order #

source

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

One (Lex α)

Equations

source

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

Zero (Lex α)

Equations

source

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

Mul (Lex α)

Equations

source

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

Add (Lex α)

Equations

source

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

Inv (Lex α)

Equations

source

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

Neg (Lex α)

Equations

source

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

Div (Lex α)

Equations

source

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

Sub (Lex α)

Equations

source

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

Pow (Lex α) β

Equations

source

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

VAdd β (Lex α)

Equations

source

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

SMul β (Lex α)

Equations

source

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

Pow α (Lex β)

Equations

source

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

VAdd (Lex β) α

Equations

source

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

SMul (Lex β) α

Equations

source

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

Semigroup (Lex α)

Equations

source

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

AddSemigroup (Lex α)

Equations

source

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

CommSemigroup (Lex α)

Equations

source

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

AddCommSemigroup (Lex α)

Equations

source

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

IsLeftCancelMul (Lex α)

source

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

IsLeftCancelAdd (Lex α)

source

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

IsRightCancelMul (Lex α)

source

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

IsRightCancelAdd (Lex α)

source

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

IsCancelMul (Lex α)

source

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

IsCancelAdd (Lex α)

source

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

LeftCancelSemigroup (Lex α)

Equations

source

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

AddLeftCancelSemigroup (Lex α)

Equations

source

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

RightCancelSemigroup (Lex α)

Equations

source

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

AddRightCancelSemigroup (Lex α)

Equations

source

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

MulOneClass (Lex α)

Equations

source

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

AddZeroClass (Lex α)

Equations

source

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

Monoid (Lex α)

Equations

source

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

AddMonoid (Lex α)

Equations

source

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

CommMonoid (Lex α)

Equations

source

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

AddCommMonoid (Lex α)

Equations

source

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

LeftCancelMonoid (Lex α)

Equations

source

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

AddLeftCancelMonoid (Lex α)

Equations

source

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

RightCancelMonoid (Lex α)

Equations

source

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

AddRightCancelMonoid (Lex α)

Equations

source

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

CancelMonoid (Lex α)

Equations

source

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

AddCancelMonoid (Lex α)

Equations

source

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

CancelCommMonoid (Lex α)

Equations

source

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

AddCancelCommMonoid (Lex α)

Equations

source

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

InvolutiveInv (Lex α)

Equations

source

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

InvolutiveNeg (Lex α)

Equations

source

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

DivInvMonoid (Lex α)

Equations

source

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

SubNegMonoid (Lex α)

Equations

source

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

DivisionMonoid (Lex α)

Equations

source

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

SubtractionMonoid (Lex α)

Equations

source

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

DivisionCommMonoid (Lex α)

Equations

source

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

SubtractionCommMonoid (Lex α)

Equations

source

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

Group (Lex α)

Equations

source

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

AddGroup (Lex α)

Equations

source

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

CommGroup (Lex α)

Equations

source

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

AddCommGroup (Lex α)

Equations

source

@[simp]

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

toLex 1 = 1

source

@[simp]

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

toLex 0 = 0

source

@[simp]

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

toLex a = 1 ↔ a = 1

source

@[simp]

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

toLex a = 0 ↔ a = 0

source

@[simp]

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

ofLex 1 = 1

source

@[simp]

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

ofLex 0 = 0

source

@[simp]

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

ofLex a = 1 ↔ a = 1

source

@[simp]

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

ofLex a = 0 ↔ a = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

toLex a⁻¹ = (toLex a)⁻¹

source

@[simp]

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

toLex (-a) = -toLex a

source

@[simp]

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

ofLex a⁻¹ = (ofLex a)⁻¹

source

@[simp]

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

ofLex (-a) = -ofLex a

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

toLex (a ^ b) = toLex a ^ b

source

@[simp]

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

toLex (b • a) = b • toLex a

source

@[simp]

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

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

source

@[simp]

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

ofLex (a ^ b) = ofLex a ^ b

source

@[simp]

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

ofLex (b • a) = b • ofLex a

source

@[simp]

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

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

source

@[simp]

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

a ^ toLex b = a ^ b

source

@[simp]

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

toLex b +ᵥ a = b +ᵥ a

source

@[simp]

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

toLex b • a = b • a

source

@[simp]

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

a ^ ofLex b = a ^ b

source

@[simp]

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

ofLex b +ᵥ a = b +ᵥ a

source

@[simp]

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

ofLex b • a = b • a

source

@[simp]

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

IsLeftRegular (toLex a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (toLex a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsLeftRegular (ofLex a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (ofLex a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsRightRegular (toLex a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (toLex a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRightRegular (ofLex a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (ofLex a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRegular (toLex a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (toLex a) ↔ IsAddRegular a

source

@[simp]

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

IsRegular (ofLex a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (ofLex a) ↔ IsAddRegular a

Colexicographical order #

source

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

One (Colex α)

Equations

source

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

Zero (Colex α)

Equations

source

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

Mul (Colex α)

Equations

source

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

Add (Colex α)

Equations

source

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

Inv (Colex α)

Equations

source

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

Neg (Colex α)

Equations

source

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

Div (Colex α)

Equations

source

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

Sub (Colex α)

Equations

source

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

Pow (Colex α) β

Equations

source

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

SMul β (Colex α)

Equations

source

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

VAdd β (Colex α)

Equations

source

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

Pow α (Colex β)

Equations

source

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

VAdd (Colex β) α

Equations

source

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

SMul (Colex β) α

Equations

source

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

Semigroup (Colex α)

Equations

source

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

AddSemigroup (Colex α)

Equations

source

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

CommSemigroup (Colex α)

Equations

source

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

AddCommSemigroup (Colex α)

Equations

source

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

IsLeftCancelMul (Colex α)

source

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

IsLeftCancelAdd (Colex α)

source

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

IsRightCancelMul (Colex α)

source

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

IsRightCancelAdd (Colex α)

source

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

IsCancelMul (Colex α)

source

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

IsCancelAdd (Colex α)

source

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

LeftCancelSemigroup (Colex α)

Equations

source

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

AddLeftCancelSemigroup (Colex α)

Equations

source

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

RightCancelSemigroup (Colex α)

Equations

source

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

AddRightCancelSemigroup (Colex α)

Equations

source

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

MulOneClass (Colex α)

Equations

source

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

AddZeroClass (Colex α)

Equations

source

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

Monoid (Colex α)

Equations

source

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

AddMonoid (Colex α)

Equations

source

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

CommMonoid (Colex α)

Equations

source

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

AddCommMonoid (Colex α)

Equations

source

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

LeftCancelMonoid (Colex α)

Equations

source

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

AddLeftCancelMonoid (Colex α)

Equations

source

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

RightCancelMonoid (Colex α)

Equations

source

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

AddRightCancelMonoid (Colex α)

Equations

source

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

CancelMonoid (Colex α)

Equations

source

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

AddCancelMonoid (Colex α)

Equations

source

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

CancelCommMonoid (Colex α)

Equations

source

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

AddCancelCommMonoid (Colex α)

Equations

source

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

InvolutiveInv (Colex α)

Equations

source

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

InvolutiveNeg (Colex α)

Equations

source

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

DivInvMonoid (Colex α)

Equations

source

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

SubNegMonoid (Colex α)

Equations

source

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

DivisionMonoid (Colex α)

Equations

source

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

SubtractionMonoid (Colex α)

Equations

source

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

DivisionCommMonoid (Colex α)

Equations

source

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

SubtractionCommMonoid (Colex α)

Equations

source

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

Group (Colex α)

Equations

source

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

AddGroup (Colex α)

Equations

source

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

CommGroup (Colex α)

Equations

source

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

AddCommGroup (Colex α)

Equations

source

@[simp]

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

toColex 1 = 1

source

@[simp]

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

toColex 0 = 0

source

@[simp]

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

toColex a = 1 ↔ a = 1

source

@[simp]

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

toColex a = 0 ↔ a = 0

source

@[simp]

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

ofColex 1 = 1

source

@[simp]

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

ofColex 0 = 0

source

@[simp]

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

ofColex a = 1 ↔ a = 1

source

@[simp]

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

ofColex a = 0 ↔ a = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

toColex a⁻¹ = (toColex a)⁻¹

source

@[simp]

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

toColex (-a) = -toColex a

source

@[simp]

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

ofColex a⁻¹ = (ofColex a)⁻¹

source

@[simp]

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

ofColex (-a) = -ofColex a

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

toColex (a ^ b) = toColex a ^ b

source

@[simp]

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

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

source

@[simp]

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

toColex (b • a) = b • toColex a

source

@[simp]

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

ofColex (a ^ b) = ofColex a ^ b

source

@[simp]

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

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

source

@[simp]

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

ofColex (b • a) = b • ofColex a

source

@[simp]

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

a ^ toColex b = a ^ b

source

@[simp]

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

toColex b • a = b • a

source

@[simp]

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

toColex b +ᵥ a = b +ᵥ a

source

@[simp]

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

a ^ ofColex b = a ^ b

source

@[simp]

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

ofColex b • a = b • a

source

@[simp]

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

ofColex b +ᵥ a = b +ᵥ a

source

@[simp]

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

IsLeftRegular (toColex a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (toColex a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsLeftRegular (ofColex a) ↔ IsLeftRegular a

source

@[simp]

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

IsAddLeftRegular (ofColex a) ↔ IsAddLeftRegular a

source

@[simp]

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

IsRightRegular (toColex a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (toColex a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRightRegular (ofColex a) ↔ IsRightRegular a

source

@[simp]

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

IsAddRightRegular (ofColex a) ↔ IsAddRightRegular a

source

@[simp]

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

IsRegular (toColex a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (toColex a) ↔ IsAddRegular a

source

@[simp]

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

IsRegular (ofColex a) ↔ IsRegular a

source

@[simp]

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

IsAddRegular (ofColex a) ↔ IsAddRegular a

Documentation

Mathlib.Algebra.Order.Group.Synonym

Group structure on the order type synonyms #

`OrderDual` #

Lexicographical order #

Colexicographical order #

Group structure on the order type synonyms #

OrderDual #

Lexicographical order #

Colexicographical order #

`OrderDual` #