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

@[simp]

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

@[simp]

theorem Equiv.mulLeft₀_apply {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : ↑(Equiv.mulLeft₀ a ha) = fun x => a * x

def Equiv.mulLeft₀ {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : Equiv.Perm G

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

Equations

• Equiv.mulLeft₀ a ha = Units.mulLeft (Units.mk0 a ha)

theorem mulLeft_bijective₀ {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : Function.Bijective ((fun x x_1 => x * x_1) a)

@[simp]

theorem Equiv.mulRight₀_apply {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : ↑(Equiv.mulRight₀ a ha) = fun x => x * a

@[simp]

theorem Equiv.mulRight₀_symm_apply {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : ↑(Equiv.mulRight₀ a ha).symm = fun x => x * a⁻¹

def Equiv.mulRight₀ {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : Equiv.Perm G

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

Equations

• Equiv.mulRight₀ a ha = Units.mulRight (Units.mk0 a ha)

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