Documentation

Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso

Multiplication by a positive element as an order isomorphism #

source
def OrderIso.mulLeft₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) :
G₀ ≃o G₀

Equiv.mulLeft₀ as an order isomorphism.

Equations
    Instances For
      source
      @[simp]
      theorem OrderIso.mulLeft₀_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) (x : G₀) :
      (mulLeft₀ a ha) x = a * x
      source
      @[simp]
      theorem OrderIso.mulLeft₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) (x : G₀) :
      (RelIso.symm (mulLeft₀ a ha)) x = a⁻¹ * x
      source
      theorem OrderIso.mulLeft₀_symm {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) :
      (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯
      source
      def OrderIso.mulRight₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) :
      G₀ ≃o G₀

      Equiv.mulRight₀ as an order isomorphism.

      Equations
        Instances For
          source
          @[simp]
          theorem OrderIso.mulRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) (x : G₀) :
          (mulRight₀ a ha) x = x * a
          source
          @[simp]
          theorem OrderIso.mulRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) (x : G₀) :
          (RelIso.symm (mulRight₀ a ha)) x = x * a⁻¹
          source
          theorem OrderIso.mulRight₀_symm {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) :
          (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯
          source
          def OrderIso.divRight₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) :
          G₀ ≃o G₀

          Equiv.divRight₀ as an order isomorphism.

          Equations
            Instances For
              source
              @[simp]
              theorem OrderIso.divRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) (x✝ : G₀) :
              (divRight₀ a ha) x✝ = x✝ / a
              source
              @[simp]
              theorem OrderIso.divRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosReflectLT G₀] (a : G₀) (ha : 0 < a) (x✝ : G₀) :
              (RelIso.symm (divRight₀ a ha)) x✝ = x✝ * a
              source
              theorem mul_inf₀ {G₀ : Type u_1} [GroupWithZero G₀] [SemilatticeInf G₀] [PosMulReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
              c * (a ⊓ b) = c * a ⊓ c * b
              source
              theorem mul_sup₀ {G₀ : Type u_1} [GroupWithZero G₀] [SemilatticeSup G₀] [PosMulReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
              c * (a ⊔ b) = c * a ⊔ c * b
              source
              theorem inf_mul₀ {G₀ : Type u_1} [GroupWithZero G₀] [SemilatticeInf G₀] [MulPosReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
              (a ⊓ b) * c = a * c ⊓ b * c
              source
              theorem sup_mul₀ {G₀ : Type u_1} [GroupWithZero G₀] [SemilatticeSup G₀] [MulPosReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
              (a ⊔ b) * c = a * c ⊔ b * c