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

@[simp]

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

@[simp]

theorem Equiv.mulLeft₀_symm_apply {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : ⇑(Equiv.symm (Equiv.mulLeft₀ a ha)) = fun (x : G) => 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.mk0 a ha).mulLeft

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

@[simp]

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

@[simp]

theorem Equiv.mulRight₀_symm_apply {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) : ⇑(Equiv.symm (Equiv.mulRight₀ a ha)) = fun (x : G) => 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.mk0 a ha).mulRight

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