Documentation

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas

Multiplication by a positive element as an order isomorphism #

@[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₀) :
@[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.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
@[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₀) :
@[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.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