Multiplication by a positive element as an order isomorphism #
def
OrderIso.mulLeft₀
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder 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' := ⋯ }
Instances For
@[simp]
theorem
OrderIso.mulLeft₀_symm_apply
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder G₀]
[PosMulMono G₀]
[PosMulReflectLE G₀]
(a : G₀)
(ha : 0 < a)
(x : G₀)
:
(RelIso.symm (OrderIso.mulLeft₀ a ha)) x = a⁻¹ * x
@[simp]
theorem
OrderIso.mulLeft₀_apply
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder G₀]
[PosMulMono G₀]
[PosMulReflectLE G₀]
(a : G₀)
(ha : 0 < a)
(x : G₀)
:
(OrderIso.mulLeft₀ a ha) x = a * x
def
OrderIso.mulRight₀
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder 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' := ⋯ }
Instances For
@[simp]
theorem
OrderIso.mulRight₀_symm_apply
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder G₀]
[MulPosMono G₀]
[MulPosReflectLE G₀]
(a : G₀)
(ha : 0 < a)
(x : G₀)
:
(RelIso.symm (OrderIso.mulRight₀ a ha)) x = x * a⁻¹
@[simp]
theorem
OrderIso.mulRight₀_apply
{G₀ : Type u_1}
[GroupWithZero G₀]
[Preorder G₀]
[MulPosMono G₀]
[MulPosReflectLE G₀]
(a : G₀)
(ha : 0 < a)
(x : G₀)
:
(OrderIso.mulRight₀ a ha) x = x * 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' := ⋯ }
Instances For
@[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 (OrderIso.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₀)
:
(OrderIso.divRight₀ a ha) x✝ = x✝ / a