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
    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) :
      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) :
          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) :
              Perm G₀

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

              Equations
                Instances For
                  source
                  @[simp]
                  theorem Equiv.divRight₀_apply {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
                  (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 (divRight₀ a ha)) x✝ = x✝ * a
                  source
                  def Equiv.divLeft₀ {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) :
                  Perm G₀

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem Equiv.divLeft₀_apply {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (ha : a ≠ 0) (x✝ : G₀) :
                      (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 (divLeft₀ a ha)) x✝ = a / x✝