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

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

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

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

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

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