Group structure on the order type synonyms

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

OrderDual

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance instAddCommGroupOrderDual {α : 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_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a

@[simp]

theorem toDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (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_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : OrderDual.toDual b • a = b • a

@[simp]

theorem toDual_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (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_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (b : βᵒᵈ) (a : α) : OrderDual.ofDual b +ᵥ a = b +ᵥ a

@[simp]

theorem ofDual_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 α)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : Lex α) : ofLex (b • a) = b • ofLex a

@[simp]

theorem ofLex_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (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_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Lex β) (a : α) : ofLex b • a = b • a

@[simp]

theorem ofLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 α)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) : toColex (b +ᵥ a) = b +ᵥ toColex a

@[simp]

theorem toColex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (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_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : toColex b • a = b • a

@[simp]

theorem toColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (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_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : Colex β) (a : α) : ofColex b • a = b • a

@[simp]

theorem ofColex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (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

@[simp]

theorem isAddRegular_ofColex {α : Type u_1} [AddMonoid α] {a : Colex α} : IsAddRegular (ofColex a) ↔ IsAddRegular a