Multiplication by a positive element as an order isomorphism

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' := ⋯ }

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

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

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⁻¹ ⋯

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' := ⋯ }

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

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

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⁻¹ ⋯

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' := ⋯ }

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

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

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

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

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

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