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.

source
@[simp]
theorem equiv.mul_left₀_apply {G : Type u_1} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.mul_left₀ a ha) = has_mul.mul a
source
@[simp]
theorem equiv.mul_left₀_symm_apply {G : Type u_1} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.symm (equiv.mul_left₀ a ha)) = has_mul.mul ↑(units.mk0 a ha)⁻¹
source
@[protected]
def equiv.mul_left₀ {G : Type u_1} [group_with_zero G] (a : G) (ha : a ≠ 0) :
equiv.perm G

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

Equations
source
theorem mul_left_bijective₀ {G : Type u_1} [group_with_zero G] (a : G) (ha : a ≠ 0) :
function.bijective (has_mul.mul a)
source
@[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
source
@[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)⁻¹
source
@[protected]
def equiv.mul_right₀ {G : Type u_1} [group_with_zero G] (a : G) (ha : a ≠ 0) :
equiv.perm G

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

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