Documentation

Mathlib.Algebra.Order.Group.OrderIso

Inverse and multiplication as order isomorphisms in ordered groups #

source
def OrderIso.inv (α : Type u) [Group α] [LE α] [MulLeftMono α] [MulRightMono α] :
α ≃o αᵒᵈ

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

Instances For
    source
    def OrderIso.neg (α : Type u) [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] :
    α ≃o αᵒᵈ

    x ↦ -x as an order-reversing equivalence.

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

      Alias of the forward direction of inv_le'.

      source
      theorem neg_le_of_neg_le {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
      -a ≤ b → -b ≤ a

      Alias of the forward direction of neg_le.

      source
      theorem le_inv' {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] {a b : α} :
      a ≤ b⁻¹ ↔ b ≤ a⁻¹
      source
      theorem le_neg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
      a ≤ -b ↔ b ≤ -a
      source
      def OrderIso.divLeft {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) :
      α ≃o αᵒᵈ

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

      Instances For
        source
        def OrderIso.subLeft {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) :
        α ≃o αᵒᵈ

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

        Instances For
          source
          @[simp]
          theorem OrderIso.subLeft_symm_apply {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a : α) (a✝ : αᵒᵈ) :
          (RelIso.symm (subLeft a)) a✝ = -OrderDual.ofDual a✝ + a
          source
          @[simp]
          theorem OrderIso.subLeft_apply {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] (a a✝ : α) :
          (subLeft a) a✝ = OrderDual.toDual (a - a✝)
          source
          @[simp]
          theorem OrderIso.divLeft_apply {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a a✝ : α) :
          (divLeft a) a✝ = OrderDual.toDual (a / a✝)
          source
          @[simp]
          theorem OrderIso.divLeft_symm_apply {α : Type u} [Group α] [LE α] [MulLeftMono α] [MulRightMono α] (a : α) (a✝ : αᵒᵈ) :
          (RelIso.symm (divLeft a)) a✝ = (OrderDual.ofDual a✝)⁻¹ * a
          source
          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'.

          source
          theorem le_neg_of_le_neg {α : Type u} [AddGroup α] [LE α] [AddLeftMono α] [AddRightMono α] {a b : α} :
          a ≤ -b → b ≤ -a

          Alias of the forward direction of le_neg.

          source
          def OrderIso.mulRight {α : Type u} [Group α] [LE α] [MulRightMono α] (a : α) :
          α ≃o α

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

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

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

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

              x ↦ x / a as an order isomorphism.

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

                x ↦ x - a as an order isomorphism.

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

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

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

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

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