# 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

- OrderIso.mulLeft₀ a ha = { toEquiv := Equiv.mulLeft₀ a ⋯, map_rel_iff' := ⋯ }

Instances For

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

- OrderIso.mulRight₀ a ha = { toEquiv := Equiv.mulRight₀ a ⋯, map_rel_iff' := ⋯ }

Instances For

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

- OrderIso.divRight₀ a ha = { toEquiv := Equiv.divRight₀ a ⋯, map_rel_iff' := ⋯ }

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