Documentation

Mathlib.Algebra.GroupWithZero.Units.Equiv

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

source
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
Instances For
    source
    @[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
    source
    @[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
    source
    theorem mulLeft_bijective₀ {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) :
    Function.Bijective fun (x : G) => a * x
    source
    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
    Instances For
      source
      @[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
      source
      @[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⁻¹
      source
      theorem mulRight_bijective₀ {G : Type u_1} [GroupWithZero G] (a : G) (ha : a ≠ 0) :
      Function.Bijective fun (x : G) => x * a