# mathlib3documentation

algebra.hom.equiv.units.group_with_zero

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]
theorem equiv.mul_left₀_apply {G : Type u_1} (a : G) (ha : a 0) :
ha) =
@[simp]
theorem equiv.mul_left₀_symm_apply {G : Type u_1} (a : G) (ha : a 0) :
@[protected]
def equiv.mul_left₀ {G : Type u_1} (a : G) (ha : a 0) :

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

Equations
theorem mul_left_bijective₀ {G : Type u_1} (a : G) (ha : a 0) :
@[simp]
theorem equiv.mul_right₀_apply {G : Type u_1} (a : G) (ha : a 0) :
ha) = λ (x : G), x * a
@[simp]
theorem equiv.mul_right₀_symm_apply {G : Type u_1} (a : G) (ha : a 0) :
(equiv.symm ha)) = λ (x : G), x * ha)⁻¹
@[protected]
def equiv.mul_right₀ {G : Type u_1} (a : G) (ha : a 0) :

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

Equations
theorem mul_right_bijective₀ {G : Type u_1} (a : G) (ha : a 0) :
function.bijective (λ (_x : G), _x * a)