# Documentation

Mathlib.Algebra.Hom.Equiv.Units.GroupWithZero

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

@[simp]
theorem Equiv.mulLeft₀_symm_apply {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
↑(Equiv.symm ()) = fun x => a⁻¹ * x
@[simp]
theorem Equiv.mulLeft₀_apply {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
↑() = fun x => a * x
def Equiv.mulLeft₀ {G : Type u_1} [inst : ] (a : G) (ha : a 0) :

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

Equations
theorem Equiv.mulLeft_bijective₀ {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
Function.Bijective ((fun x x_1 => x * x_1) a)
@[simp]
theorem Equiv.mulRight₀_symm_apply {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
↑(Equiv.symm ()) = fun x => x * a⁻¹
@[simp]
theorem Equiv.mulRight₀_apply {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
↑() = fun x => x * a
def Equiv.mulRight₀ {G : Type u_1} [inst : ] (a : G) (ha : a 0) :

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

Equations
theorem Equiv.mulRight_bijective₀ {G : Type u_1} [inst : ] (a : G) (ha : a 0) :
Function.Bijective fun x => x * a