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
      source
      def Equiv.divRight₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
      G₀ ≃ G₀

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

      Equations
      • Equiv.divRight₀ a ha = { toFun := fun (x : G₀) => x / a, invFun := fun (x : G₀) => x * a, left_inv := ⋯, right_inv := ⋯ }
      Instances For
        source
        @[simp]
        theorem Equiv.divRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
        (Equiv.divRight₀ a ha).symm x✝ = x✝ * a
        source
        @[simp]
        theorem Equiv.divRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
        (Equiv.divRight₀ a ha) x✝ = x✝ / a