Group structure on the order type synonyms

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

OrderDual

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

Equations

• instOneOrderDual = h

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

Equations

• instZeroOrderDual = h

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

Equations

• instMulOrderDual = h

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

Equations

• instAddOrderDual = h

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

Equations

• instInvOrderDual = h

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

Equations

• instNegOrderDual = h

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

Equations

• instDivOrderDual = h

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

Equations

• instSubOrderDual = h

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

Equations

• OrderDual.instPow = h

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

Equations

• OrderDual.instSMul = h

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

Equations

• OrderDual.instVAdd = h

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

Equations

• OrderDual.instPow' = h

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

Equations

• OrderDual.instVAdd' = h

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

Equations

• OrderDual.instSMul' = h

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

Equations

• instSemigroupOrderDual = h

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

Equations

• instAddSemigroupOrderDual = h

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

Equations

• instCommSemigroupOrderDual = h

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

Equations

• instAddCommSemigroupOrderDual = h

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

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

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

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

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

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

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

Equations

• instLeftCancelSemigroupOrderDual = h

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

Equations

• instAddLeftCancelSemigroupOrderDual = h

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

Equations

• instRightCancelSemigroupOrderDual = h

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

Equations

• instAddRightCancelSemigroupOrderDual = h

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

Equations

• instMulOneClassOrderDual = h

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

Equations

• instAddZeroClassOrderDual = h

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

Equations

• instMonoidOrderDual = h

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

Equations

• instAddMonoidOrderDual = h

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

Equations

• OrderDual.instCommMonoid = h

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

Equations

• OrderDual.instAddCommMonoid = h

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

Equations

• instLeftCancelMonoidOrderDual = h

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

Equations

• instAddLeftCancelMonoidOrderDual = h

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

Equations

• instRightCancelMonoidOrderDual = h

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

Equations

• instAddRightCancelMonoidOrderDual = h

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

Equations

• instCancelMonoidOrderDual = h

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

Equations

• instAddCancelMonoidOrderDual = h

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

Equations

• OrderDual.instCancelCommMonoid = h

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

Equations

• OrderDual.instAddCancelCommMonoid = h

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

Equations

• instInvolutiveInvOrderDual = h

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

Equations

• instInvolutiveNegOrderDual = h

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

Equations

• instDivInvMonoidOrderDual = h

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

Equations

• instSubNegAddMonoidOrderDual = h

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

Equations

• instDivisionMonoidOrderDual = h

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

Equations

• instSubtractionMonoidOrderDual = h

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

Equations

• instDivisionCommMonoidOrderDual = h

instance OrderDual.subtractionCommMonoid {α : Type u_1} [h : SubtractionCommMonoid α] : SubtractionCommMonoid αᵒᵈ

Equations

• OrderDual.subtractionCommMonoid = h

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

Equations

• OrderDual.instGroup = h

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

Equations

• OrderDual.instAddGroup = h

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

Equations

• instCommGroupOrderDual = h

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

Equations

• instAddCommGroupOrderDual = h

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

@[simp]

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

Lexicographical order

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

Equations

• instOneLex = h

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

Equations

• instZeroLex = h

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

Equations

• instMulLex = h

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

Equations

• instAddLex = h

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

Equations

• instInvLex = h

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

Equations

• instNegLex = h

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

Equations

• instDivLex = h

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

Equations

• instSubLex = h

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

Equations

• Lex.instPow = h

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

Equations

• Lex.instVAdd = h

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

Equations

• Lex.instSMul = h

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

Equations

• Lex.instPow' = h

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

Equations

• Lex.instVAdd' = h

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

Equations

• Lex.instSMul' = h

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

Equations

• instSemigroupLex = h

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

Equations

• instAddSemigroupLex = h

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

Equations

• instCommSemigroupLex = h

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

Equations

• instAddCommSemigroupLex = h

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

instance instIsAddLeftCancelLex {α : Type u_1} [Add α] [IsLeftCancelAdd α] : IsLeftCancelAdd (Lex α)

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

instance instIsAddRightCancelLex {α : Type u_1} [Add α] [IsRightCancelAdd α] : IsRightCancelAdd (Lex α)

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

instance instIsAddCancelLex {α : Type u_1} [Add α] [IsCancelAdd α] : IsCancelAdd (Lex α)

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

Equations

• instLeftCancelSemigroupLex = h

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

Equations

• instAddLeftCancelSemigroupLex = h

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

Equations

• instRightCancelSemigroupLex = h

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

Equations

• instAddRightCancelSemigroupLex = h

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

Equations

• instMulOneClassLex = h

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

Equations

• instAddZeroClassLex = h

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

Equations

• instMonoidLex = h

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

Equations

• instAddMonoidLex = h

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

Equations

• instCommMonoidLex = h

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

Equations

• instAddCommMonoidLex = h

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

Equations

• instLeftCancelMonoidLex = h

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

Equations

• instAddLeftCancelMonoidLex = h

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

Equations

• instRightCancelMonoidLex = h

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

Equations

• instAddRightCancelMonoidLex = h

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

Equations

• instCancelMonoidLex = h

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

Equations

• instAddCancelMonoidLex = h

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

Equations

• instCancelCommMonoidLex = h

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

Equations

• instAddCancelCommMonoidLex = h

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

Equations

• instInvolutiveInvLex = h

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

Equations

• instInvolutiveNegLex = h

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

Equations

• instDivInvMonoidLex = h

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

Equations

• instSubNegAddMonoidLex = h

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

Equations

• instDivisionMonoidLex = h

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

Equations

• instSubtractionMonoidLex = h

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

Equations

• instDivisionCommMonoidLex = h

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

Equations

• instGroupLex = h

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

Equations

• instAddGroupLex = h

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

Equations

• instCommGroupLex = h

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

Equations

• instAddCommGroupLex = h

@[simp]

theorem toLex_one {α : Type u_1} [One α] : toLex 1 = 1

@[simp]

theorem toLex_zero {α : Type u_1} [Zero α] : toLex 0 = 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 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_smul {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) : toLex (b • a) = b • toLex a

@[simp]

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