Documentation

Mathlib.Algebra.Order.Group.Synonym

Group structure on the order type synonyms #

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

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 instIsAddLeftCancelOrderDual {α : Type u_1} [Add α] [h : IsLeftCancelAdd α] :
                                      IsLeftCancelAdd αᵒᵈ
                                      source
                                      instance instIsRightCancelMulOrderDual {α : Type u_1} [Mul α] [h : IsRightCancelMul α] :
                                      IsRightCancelMul αᵒᵈ
                                      source
                                      instance instIsAddRightCancelOrderDual {α : Type u_1} [Add α] [h : IsRightCancelAdd α] :
                                      IsRightCancelAdd αᵒᵈ
                                      source
                                      instance instIsCancelMulOrderDual {α : Type u_1} [Mul α] [h : IsCancelMul α] :
                                      IsCancelMul αᵒᵈ
                                      source
                                      instance instIsAddCancelOrderDual {α : 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_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_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
                                                                                                  OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
                                                                                                  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 ofDual_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵒᵈ) (b : β) :
                                                                                                  OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b
                                                                                                  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 ofDual_smul {β : Type u_2} {α : Type u_1} [SMul β α] (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

                                                                                                  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.instSMul {β : Type u_2} {α : Type u_1} [h : SMul β α] :
                                                                                                                    SMul β (Lex α)
                                                                                                                    Equations
                                                                                                                      source
                                                                                                                      instance Lex.instVAdd {β : Type u_2} {α : Type u_1} [h : VAdd β α] :
                                                                                                                      VAdd β (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 instIsAddLeftCancelLex {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
                                                                                                                                      IsLeftCancelAdd (Lex α)
                                                                                                                                      source
                                                                                                                                      instance instIsRightCancelMulLex {α : Type u_1} [Mul α] [IsRightCancelMul α] :
                                                                                                                                      IsRightCancelMul (Lex α)
                                                                                                                                      source
                                                                                                                                      instance instIsAddRightCancelLex {α : Type u_1} [Add α] [IsRightCancelAdd α] :
                                                                                                                                      IsRightCancelAdd (Lex α)
                                                                                                                                      source
                                                                                                                                      instance instIsCancelMulLex {α : Type u_1} [Mul α] [IsCancelMul α] :
                                                                                                                                      IsCancelMul (Lex α)
                                                                                                                                      source
                                                                                                                                      instance instIsAddCancelLex {α : 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 ofLex_one {α : Type u_1} [One α] :
                                                                                                                                                                                                  ofLex 1 = 1
                                                                                                                                                                                                  source
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem ofLex_zero {α : Type u_1} [Zero α] :
                                                                                                                                                                                                  ofLex 0 = 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_vadd {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : Lex α) :
                                                                                                                                                                                                  ofLex (b +ᵥ a) = b +ᵥ ofLex a
                                                                                                                                                                                                  source
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem ofLex_smul {β : Type u_2} {α : Type u_1} [SMul β α] (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_smul' {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
                                                                                                                                                                                                  toLex b • a = b • a
                                                                                                                                                                                                  source
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem toLex_vadd' {β : Type u_2} {α : Type u_1} [VAdd β α] (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