Documentation

Mathlib.Algebra.Order.Group.OrderIso

Inverse and multiplication as order isomorphisms in ordered groups #

def OrderIso.inv (α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] :

x ↦ x⁻¹ as an order-reversing equivalence.

Equations
    Instances For
      def OrderIso.neg (α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] :

      x ↦ -x as an order-reversing equivalence.

      Equations
        Instances For
          @[simp]
          theorem OrderIso.neg_symm_apply (α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a✝ : αᵒᵈ) :
          @[simp]
          theorem OrderIso.inv_apply (α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a✝ : α) :
          (inv α) a✝ = OrderDual.toDual a✝⁻¹
          @[simp]
          theorem OrderIso.inv_symm_apply (α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a✝ : αᵒᵈ) :
          @[simp]
          theorem OrderIso.neg_apply (α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a✝ : α) :
          (neg α) a✝ = OrderDual.toDual (-a✝)
          theorem inv_le' {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} :
          theorem neg_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
          -a b -b a
          theorem inv_le_of_inv_le' {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} :
          a⁻¹ bb⁻¹ a

          Alias of the forward direction of inv_le'.

          theorem neg_le_of_neg_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
          -a b-b a
          theorem le_inv' {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} :
          theorem le_neg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
          a -b b -a
          def OrderIso.divLeft {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) :

          x ↦ a / x as an order-reversing equivalence.

          Equations
            Instances For
              def OrderIso.subLeft {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) :

              x ↦ a - x as an order-reversing equivalence.

              Equations
                Instances For
                  @[simp]
                  theorem OrderIso.divLeft_apply {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a a✝ : α) :
                  (divLeft a) a✝ = OrderDual.toDual (a / a✝)
                  @[simp]
                  theorem OrderIso.subLeft_apply {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a a✝ : α) :
                  (subLeft a) a✝ = OrderDual.toDual (a - a✝)
                  @[simp]
                  theorem OrderIso.subLeft_symm_apply {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) (a✝ : αᵒᵈ) :
                  @[simp]
                  theorem OrderIso.divLeft_symm_apply {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) (a✝ : αᵒᵈ) :
                  theorem le_inv_of_le_inv {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} :
                  a b⁻¹b a⁻¹

                  Alias of the forward direction of le_inv'.

                  theorem le_neg_of_le_neg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
                  a -bb -a
                  def OrderIso.mulRight {α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) :
                  α ≃o α

                  Equiv.mulRight as an OrderIso. See also OrderEmbedding.mulRight.

                  Equations
                    Instances For
                      def OrderIso.addRight {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) :
                      α ≃o α

                      Equiv.addRight as an OrderIso. See also OrderEmbedding.addRight.

                      Equations
                        Instances For
                          @[simp]
                          theorem OrderIso.mulRight_apply {α : Type u} [Group α] [LE α] [MulRightMono α] (a x : α) :
                          (mulRight a) x = x * a
                          @[simp]
                          theorem OrderIso.addRight_toEquiv {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) :
                          @[simp]
                          theorem OrderIso.mulRight_toEquiv {α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) :
                          @[simp]
                          theorem OrderIso.addRight_apply {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a x : α) :
                          (addRight a) x = x + a
                          @[simp]
                          theorem OrderIso.mulRight_symm {α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) :
                          @[simp]
                          theorem OrderIso.addRight_symm {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) :
                          def OrderIso.divRight {α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) :
                          α ≃o α

                          x ↦ x / a as an order isomorphism.

                          Equations
                            Instances For
                              def OrderIso.subRight {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a : α) :
                              α ≃o α

                              x ↦ x - a as an order isomorphism.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem OrderIso.divRight_apply {α : Type u} [Group α] [LE α] [MulRightMono α] (a b : α) :
                                  (divRight a) b = b / a
                                  @[simp]
                                  theorem OrderIso.subRight_symm_apply {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a b : α) :
                                  (RelIso.symm (subRight a)) b = b + a
                                  @[simp]
                                  theorem OrderIso.subRight_apply {α : Type u} [AddGroup α] [LE α] [AddRightMono α] (a b : α) :
                                  (subRight a) b = b - a
                                  @[simp]
                                  theorem OrderIso.divRight_symm_apply {α : Type u} [Group α] [LE α] [MulRightMono α] (a b : α) :
                                  (RelIso.symm (divRight a)) b = b * a
                                  def OrderIso.mulLeft {α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) :
                                  α ≃o α

                                  Equiv.mulLeft as an OrderIso. See also OrderEmbedding.mulLeft.

                                  Equations
                                    Instances For
                                      def OrderIso.addLeft {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) :
                                      α ≃o α

                                      Equiv.addLeft as an OrderIso. See also OrderEmbedding.addLeft.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem OrderIso.mulLeft_apply {α : Type u} [Group α] [LE α] [MulLeftMono α] (a x : α) :
                                          (mulLeft a) x = a * x
                                          @[simp]
                                          theorem OrderIso.mulLeft_toEquiv {α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) :
                                          @[simp]
                                          theorem OrderIso.addLeft_toEquiv {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) :
                                          @[simp]
                                          theorem OrderIso.addLeft_apply {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a x : α) :
                                          (addLeft a) x = a + x
                                          @[simp]
                                          theorem OrderIso.mulLeft_symm {α : Type u} [Group α] [LE α] [MulLeftMono α] (a : α) :
                                          @[simp]
                                          theorem OrderIso.addLeft_symm {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] (a : α) :