Multiplication by a positive element as an order isomorphism

def OrderIso.mulLeft₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulMono G₀] [PosMulReflectLE 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₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulMono G₀] [PosMulReflectLE G₀] (a : G₀) (ha : 0 < a) (x : G₀) : (RelIso.symm (mulLeft₀ a ha)) x = a⁻¹ * x

@[simp]

theorem OrderIso.mulLeft₀_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulMono G₀] [PosMulReflectLE G₀] (a : G₀) (ha : 0 < a) (x : G₀) : (mulLeft₀ a ha) x = a * x

theorem OrderIso.mulLeft₀_symm {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [PosMulMono G₀] [PosMulReflectLE G₀] [ZeroLEOneClass G₀] (a : G₀) (ha : 0 < a) : (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯

def OrderIso.mulRight₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosMono G₀] [MulPosReflectLE 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₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosMono G₀] [MulPosReflectLE G₀] (a : G₀) (ha : 0 < a) (x : G₀) : (RelIso.symm (mulRight₀ a ha)) x = x * a⁻¹

@[simp]

theorem OrderIso.mulRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosMono G₀] [MulPosReflectLE G₀] (a : G₀) (ha : 0 < a) (x : G₀) : (mulRight₀ a ha) x = x * a

theorem OrderIso.mulRight₀_symm {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [MulPosMono G₀] [MulPosReflectLE G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) : (mulRight₀ a ha).symm = mulRight₀ a⁻¹ ⋯

def OrderIso.divRight₀ {G₀ : Type u_1} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [MulPosStrictMono G₀] [MulPosReflectLE G₀] [PosMulReflectLT 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₀] [ZeroLEOneClass G₀] [MulPosStrictMono G₀] [MulPosReflectLE G₀] [PosMulReflectLT 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₀] [ZeroLEOneClass G₀] [MulPosStrictMono G₀] [MulPosReflectLE G₀] [PosMulReflectLT G₀] (a : G₀) (ha : 0 < a) (x✝ : G₀) : (divRight₀ a ha) x✝ = x✝ / a