mathlib3 documentation

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} [group_with_zero G] (a : G) (ha : a 0) :
@[simp]
@[protected]
def equiv.mul_left₀ {G : Type u_1} [group_with_zero G] (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} [group_with_zero G] (a : G) (ha : a 0) :
@[simp]
theorem equiv.mul_right₀_apply {G : Type u_1} [group_with_zero G] (a : G) (ha : a 0) :
(equiv.mul_right₀ a ha) = λ (x : G), x * a
@[simp]
theorem equiv.mul_right₀_symm_apply {G : Type u_1} [group_with_zero G] (a : G) (ha : a 0) :
(equiv.symm (equiv.mul_right₀ a ha)) = λ (x : G), x * (units.mk0 a ha)⁻¹
@[protected]
def equiv.mul_right₀ {G : Type u_1} [group_with_zero G] (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} [group_with_zero G] (a : G) (ha : a 0) :
function.bijective (λ (_x : G), _x * a)