Documentation

Mathlib.Algebra.GroupWithZero.Units.Equiv

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

source
def unitsEquivNeZero {G₀ : Type u_1} [GroupWithZero G₀] :
G₀ˣ ≃ { a : G₀ // a ≠ 0 }

In a GroupWithZero G₀, the unit group G₀ˣ is equivalent to the subtype of nonzero elements.

Equations
  • unitsEquivNeZero = { toFun := fun (a : G₀ˣ) => ⟨↑a, ⋯⟩, invFun := fun (a : { a : G₀ // a ≠ 0 }) => Units.mk0 ↑a ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
    source
    @[simp]
    theorem unitsEquivNeZero_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : { a : G₀ // a ≠ 0 }) :
    unitsEquivNeZero.symm a = Units.mk0 ↑a ⋯
    source
    @[simp]
    theorem unitsEquivNeZero_apply_coe {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀ˣ) :
    ↑(unitsEquivNeZero a) = ↑a
    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) :
        Equiv.Perm 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₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
          (Equiv.divRight₀ a ha) x✝ = x✝ / a
          source
          @[simp]
          theorem Equiv.divRight₀_symm_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
          (Equiv.symm (Equiv.divRight₀ a ha)) x✝ = x✝ * a
          source
          def Equiv.divLeft₀ {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
          Equiv.Perm G₀

          Left division by a nonzero element in a CommGroupWithZero is a permutation of the underlying type.

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