Documentation

Mathlib.Algebra.GroupWithZero.Units.Equiv

Multiplication by a nonzero element in a GroupWithZero is a permutation. #

source
def unitsEquivNeZero {G₀ : Type u_1} [GroupWithZero G₀] :
G₀ˣ ≃ { a : G₀ // a ≠ 0 }

In a GroupWithZero G₀, the unit group G₀ˣ is equivalent to the subtype of nonzero elements.

Equations
source
@[simp]
theorem unitsEquivNeZero_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : { a : G₀ // a ≠ 0 }) :
unitsEquivNeZero.symm a = Units.mk0 ↑a ⋯
source
@[simp]
theorem unitsEquivNeZero_apply_coe {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀ˣ) :
↑(unitsEquivNeZero a) = ↑a
source
def Equiv.mulLeft₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Perm G₀

Left multiplication by a nonzero element in a GroupWithZero is a permutation of the underlying type.

Equations
source
@[simp]
theorem Equiv.mulLeft₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
⇑(Equiv.mulLeft₀ a ha) = fun (x : G₀) => a * x
source
@[simp]
theorem Equiv.mulLeft₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
⇑(Equiv.symm (Equiv.mulLeft₀ a ha)) = fun (x : G₀) => a⁻¹ * x
source
theorem mulLeft_bijective₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Function.Bijective fun (x : G₀) => a * x
source
def Equiv.mulRight₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Perm G₀

Right multiplication by a nonzero element in a GroupWithZero is a permutation of the underlying type.

Equations
source
@[simp]
theorem Equiv.mulRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
⇑(Equiv.mulRight₀ a ha) = fun (x : G₀) => x * a
source
@[simp]
theorem Equiv.mulRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
⇑(Equiv.symm (Equiv.mulRight₀ a ha)) = fun (x : G₀) => x * a⁻¹
source
theorem mulRight_bijective₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Function.Bijective fun (x : G₀) => x * a
source
def Equiv.divRight₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Perm G₀

Right division by a nonzero element in a GroupWithZero is a permutation of the underlying type.

Equations
  • Equiv.divRight₀ a ha = { toFun := fun (x : G₀) => x / a, invFun := fun (x : G₀) => x * a, left_inv := ⋯, right_inv := ⋯ }
source
@[simp]
theorem Equiv.divRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
(divRight₀ a ha) x✝ = x✝ / a
source
@[simp]
theorem Equiv.divRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
(Equiv.symm (divRight₀ a ha)) x✝ = x✝ * a
source
def Equiv.divLeft₀ {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
Perm G₀

Left division by a nonzero element in a CommGroupWithZero is a permutation of the underlying type.

Equations
  • Equiv.divLeft₀ a ha = { toFun := fun (x : G₀) => a / x, invFun := fun (x : G₀) => a / x, left_inv := ⋯, right_inv := ⋯ }
source
@[simp]
theorem Equiv.divLeft₀_apply {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
(divLeft₀ a ha) x✝ = a / x✝
source
@[simp]
theorem Equiv.divLeft₀_symm_apply {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
(Equiv.symm (divLeft₀ a ha)) x✝ = a / x✝