Group structure on the order type synonyms

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

OrderDual

@[implicit_reducible]

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

Equations

• OrderDual.instOne = h

@[implicit_reducible]

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

Equations

• OrderDual.instZero = h

@[implicit_reducible]

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

Equations

• OrderDual.instMul = h

@[implicit_reducible]

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

Equations

• OrderDual.instAdd = h

@[implicit_reducible]

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

Equations

• OrderDual.instInv = h

@[implicit_reducible]

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

Equations

• OrderDual.instNeg = h

@[implicit_reducible]

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

Equations

• OrderDual.instDiv = h

@[implicit_reducible]

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

Equations

• OrderDual.instSub = h

@[implicit_reducible]

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

Equations

• OrderDual.instPow = h

@[implicit_reducible]

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

Equations

• OrderDual.instVAdd = h

@[implicit_reducible]

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

Equations

• OrderDual.instSMul = h

@[implicit_reducible]

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

Equations

• OrderDual.instPow_1 = h

@[implicit_reducible]

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

Equations

• OrderDual.instSMul' = h

@[implicit_reducible]

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

Equations

• OrderDual.instVAdd' = h

@[implicit_reducible]

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

Equations

• OrderDual.instSemigroup = { toMul := OrderDual.instMul, mul_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddSemigroup = { toAdd := OrderDual.instAdd, add_assoc := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCommSemigroup = { toSemigroup := OrderDual.instSemigroup, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCommSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, add_comm := ⋯ }

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 αᵒᵈ

Equations

• OrderDual.instLeftCancelSemigroup = { toSemigroup := OrderDual.instSemigroup, toIsLeftCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddLeftCancelSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, toIsLeftCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instRightCancelSemigroup = { toSemigroup := OrderDual.instSemigroup, toIsRightCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddRightCancelSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, toIsRightCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instMulOneClass = { toOne := OrderDual.instOne, toMul := OrderDual.instMul, one_mul := ⋯, mul_one := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddZeroClass = { toZero := OrderDual.instZero, toAdd := OrderDual.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instMonoid = { toSemigroup := OrderDual.instSemigroup, toOne := OrderDual.instMulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := Monoid.npow, npow_zero := ⋯, npow_succ := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instCommMonoid = { toMonoid := OrderDual.instMonoid, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCommMonoid = { toAddMonoid := OrderDual.instAddMonoid, add_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instLeftCancelMonoid = { toMonoid := OrderDual.instMonoid, toIsLeftCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddLeftCancelMonoid = { toAddMonoid := OrderDual.instAddMonoid, toIsLeftCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instRightCancelMonoid = { toMonoid := OrderDual.instMonoid, toIsRightCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddRightCancelMonoid = { toAddMonoid := OrderDual.instAddMonoid, toIsRightCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCancelMonoid = { toLeftCancelMonoid := OrderDual.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCancelMonoid = { toAddLeftCancelMonoid := OrderDual.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCancelCommMonoid = { toCommMonoid := OrderDual.instCommMonoid, toIsLeftCancelMul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCancelCommMonoid = { toAddCommMonoid := OrderDual.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instInvolutiveInv = { toInv := OrderDual.instInv, inv_inv := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instInvolutiveNeg = { toNeg := OrderDual.instNeg, neg_neg := ⋯ }

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

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

Equations

• OrderDual.instDivisionMonoid = { toDivInvMonoid := OrderDual.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instSubtractionMonoid = { toSubNegMonoid := OrderDual.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instDivisionCommMonoid = { toDivisionMonoid := OrderDual.instDivisionMonoid, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instDivisionAddCommMonoid = { toSubtractionMonoid := OrderDual.instSubtractionMonoid, add_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instGroup = { toDivInvMonoid := OrderDual.instDivInvMonoid, inv_mul_cancel := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddGroup = { toSubNegMonoid := OrderDual.instSubNegAddMonoid, neg_add_cancel := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instCommGroup = { toGroup := OrderDual.instGroup, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• OrderDual.instAddCommGroup = { toAddGroup := OrderDual.instAddGroup, add_comm := ⋯ }

@[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_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_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_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

@[implicit_reducible]

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

Equations

• instOneLex = h

@[implicit_reducible]

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

Equations

• instZeroLex = h

@[implicit_reducible]

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

Equations

• instMulLex = h

@[implicit_reducible]

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

Equations

• instAddLex = h

@[implicit_reducible]

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

Equations

• instInvLex = h

@[implicit_reducible]

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

Equations

• instNegLex = h

@[implicit_reducible]

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

Equations

• instDivLex = h

@[implicit_reducible]

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

Equations

• instSubLex = h

@[implicit_reducible]

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

Equations

• Lex.instPow = h

@[implicit_reducible]

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

Equations

• Lex.instVAdd = h

@[implicit_reducible]

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

Equations

• Lex.instSMul = h

@[implicit_reducible]

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

Equations

• Lex.instPow' = h

@[implicit_reducible]

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

Equations

• Lex.instVAdd' = h

@[implicit_reducible]

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

Equations

• Lex.instSMul' = h

@[implicit_reducible]

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

Equations

• instSemigroupLex = h

@[implicit_reducible]

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

Equations

• instAddSemigroupLex = h

@[implicit_reducible]

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

Equations

• instCommSemigroupLex = h

@[implicit_reducible]

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

Equations

• instAddCommSemigroupLex = h

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

Equations

• instLeftCancelSemigroupLex = h

@[implicit_reducible]

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

Equations

• instAddLeftCancelSemigroupLex = h

@[implicit_reducible]

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

Equations

• instRightCancelSemigroupLex = h

@[implicit_reducible]

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

Equations

• instAddRightCancelSemigroupLex = h

@[implicit_reducible]

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

Equations

• instMulOneClassLex = h

@[implicit_reducible]

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

Equations

• instAddZeroClassLex = h

@[implicit_reducible]

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

Equations

• instMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddMonoidLex = h

@[implicit_reducible]

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

Equations

• instCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instLeftCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddLeftCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instRightCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddRightCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddCancelMonoidLex = h

@[implicit_reducible]

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

Equations

• instCancelCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instAddCancelCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instInvolutiveInvLex = h

@[implicit_reducible]

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

Equations

• instInvolutiveNegLex = h

@[implicit_reducible]

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

Equations

• instDivInvMonoidLex = h

@[implicit_reducible]

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

Equations

• instSubNegAddMonoidLex = h

@[implicit_reducible]

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

Equations

• instDivisionMonoidLex = h

@[implicit_reducible]

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

Equations

• instSubtractionMonoidLex = h

@[implicit_reducible]

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

Equations

• instDivisionCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instDivisionAddCommMonoidLex = h

@[implicit_reducible]

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

Equations

• instGroupLex = h

@[implicit_reducible]

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

Equations

• instAddGroupLex = h

@[implicit_reducible]

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

Equations

• instCommGroupLex = h

@[implicit_reducible]

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 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_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_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_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

@[implicit_reducible]

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

Equations

• instOneColex = h

@[implicit_reducible]

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

Equations

• instZeroColex = h

@[implicit_reducible]

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

Equations

• instMulColex = h

@[implicit_reducible]

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

Equations

• instAddColex = h

@[implicit_reducible]

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

Equations

• instInvColex = h

@[implicit_reducible]

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

Equations

• instNegColex = h

@[implicit_reducible]

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

Equations

• instDivColex = h

@[implicit_reducible]

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

Equations

• instSubColex = h

@[implicit_reducible]

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

Equations

• Colex.instPow = h

@[implicit_reducible]

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

Equations

• Colex.instVAdd = h

@[implicit_reducible]

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

Equations

• Colex.instSMul = h

@[implicit_reducible]

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

Equations

• Colex.instPow' = h

@[implicit_reducible]

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

Equations

• Colex.instVAdd' = h

@[implicit_reducible]

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

Equations

• Colex.instSMul' = h

@[implicit_reducible]

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

Equations

• instSemigroupColex = h

@[implicit_reducible]

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

Equations

• instAddSemigroupColex = h

@[implicit_reducible]

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

Equations

• instCommSemigroupColex = h

@[implicit_reducible]

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

Equations

• instAddCommSemigroupColex = h

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

Equations

• instLeftCancelSemigroupColex = h

@[implicit_reducible]

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

Equations

• instAddLeftCancelSemigroupColex = h

@[implicit_reducible]

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

Equations

• instRightCancelSemigroupColex = h

@[implicit_reducible]

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

Equations

• instAddRightCancelSemigroupColex = h

@[implicit_reducible]

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

Equations

• instMulOneClassColex = h

@[implicit_reducible]

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

Equations

• instAddZeroClassColex = h

@[implicit_reducible]

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

Equations

• instMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddMonoidColex = h

@[implicit_reducible]

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

Equations

• instCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instLeftCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddLeftCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instRightCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddRightCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddCancelMonoidColex = h

@[implicit_reducible]

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

Equations

• instCancelCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instAddCancelCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instInvolutiveInvColex = h

@[implicit_reducible]

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

Equations

• instInvolutiveNegColex = h

@[implicit_reducible]

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

Equations

• instDivInvMonoidColex = h

@[implicit_reducible]

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

Equations

• instSubNegAddMonoidColex = h

@[implicit_reducible]

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

Equations

• instDivisionMonoidColex = h

@[implicit_reducible]

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

Equations

• instSubtractionMonoidColex = h

@[implicit_reducible]

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

Equations

• instDivisionCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instDivisionAddCommMonoidColex = h

@[implicit_reducible]

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

Equations

• instGroupColex = h

@[implicit_reducible]

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

Equations

• instAddGroupColex = h

@[implicit_reducible]

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

Equations

• instCommGroupColex = h

@[implicit_reducible]

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

Equations

• instAddCommGroupColex = h

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

@[simp]

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

@[simp]

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