Documentation

Mathlib.Algebra.GroupWithZero.Units.Equiv

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) :

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

Equations
Instances For
    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) :

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

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