Documentation

Mathlib.Algebra.Group.Units.Equiv

Multiplicative and additive equivalence acting on units. #

def toUnits {G : Type u_5} [Group G] :
G ≃* Gˣ

A group is isomorphic to its group of units.

Equations
    Instances For
      def toAddUnits {G : Type u_5} [AddGroup G] :

      An additive group is isomorphic to its group of additive units

      Equations
        Instances For
          @[simp]
          theorem val_toUnits_apply {G : Type u_5} [Group G] (x : G) :
          (toUnits x) = x
          @[simp]
          theorem val_toAddUnits_apply {G : Type u_5} [AddGroup G] (x : G) :
          (toAddUnits x) = x
          @[simp]
          theorem toAddUnits_symm_apply {G : Type u_5} [AddGroup G] (x : AddUnits G) :
          @[simp]
          theorem toUnits_symm_apply {G : Type u_5} [Group G] (x : Gˣ) :
          toUnits.symm x = x
          @[simp]
          theorem toUnits_val_apply {G : Type u_6} [Group G] (x : Gˣ) :
          toUnits x = x
          @[simp]
          theorem toAddUnits_val_apply {G : Type u_6} [AddGroup G] (x : AddUnits G) :
          toAddUnits x = x
          def Units.mapEquiv {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (h : M ≃* N) :

          A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

          Equations
            Instances For
              @[simp]
              theorem Units.mapEquiv_symm {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (h : M ≃* N) :
              @[simp]
              theorem Units.coe_mapEquiv {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (h : M ≃* N) (x : Mˣ) :
              ((mapEquiv h) x) = h x
              def Units.mulLeft {M : Type u_3} [Monoid M] (u : Mˣ) :

              Left multiplication by a unit of a monoid is a permutation of the underlying type.

              Equations
                Instances For
                  def AddUnits.addLeft {M : Type u_3} [AddMonoid M] (u : AddUnits M) :

                  Left addition of an additive unit is a permutation of the underlying type.

                  Equations
                    Instances For
                      @[simp]
                      theorem Units.mulLeft_apply {M : Type u_3} [Monoid M] (u : Mˣ) :
                      u.mulLeft = fun (x : M) => u * x
                      @[simp]
                      theorem AddUnits.addLeft_apply {M : Type u_3} [AddMonoid M] (u : AddUnits M) :
                      u.addLeft = fun (x : M) => u + x
                      @[simp]
                      theorem Units.mulLeft_symm {M : Type u_3} [Monoid M] (u : Mˣ) :
                      @[simp]
                      theorem Units.mulLeft_bijective {M : Type u_3} [Monoid M] (a : Mˣ) :
                      Function.Bijective fun (x : M) => a * x
                      theorem AddUnits.addLeft_bijective {M : Type u_3} [AddMonoid M] (a : AddUnits M) :
                      Function.Bijective fun (x : M) => a + x
                      def Units.mulRight {M : Type u_3} [Monoid M] (u : Mˣ) :

                      Right multiplication by a unit of a monoid is a permutation of the underlying type.

                      Equations
                        Instances For
                          def AddUnits.addRight {M : Type u_3} [AddMonoid M] (u : AddUnits M) :

                          Right addition of an additive unit is a permutation of the underlying type.

                          Equations
                            Instances For
                              @[simp]
                              theorem Units.mulRight_apply {M : Type u_3} [Monoid M] (u : Mˣ) :
                              u.mulRight = fun (x : M) => x * u
                              @[simp]
                              theorem AddUnits.addRight_apply {M : Type u_3} [AddMonoid M] (u : AddUnits M) :
                              u.addRight = fun (x : M) => x + u
                              @[simp]
                              @[simp]
                              theorem Units.mulRight_bijective {M : Type u_3} [Monoid M] (a : Mˣ) :
                              Function.Bijective fun (x : M) => x * a
                              theorem AddUnits.addRight_bijective {M : Type u_3} [AddMonoid M] (a : AddUnits M) :
                              Function.Bijective fun (x : M) => x + a
                              def Equiv.mulLeft {G : Type u_5} [Group G] (a : G) :

                              Left multiplication in a Group is a permutation of the underlying type.

                              Equations
                                Instances For
                                  def Equiv.addLeft {G : Type u_5} [AddGroup G] (a : G) :

                                  Left addition in an AddGroup is a permutation of the underlying type.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Equiv.coe_mulLeft {G : Type u_5} [Group G] (a : G) :
                                      (Equiv.mulLeft a) = fun (x : G) => a * x
                                      @[simp]
                                      theorem Equiv.coe_addLeft {G : Type u_5} [AddGroup G] (a : G) :
                                      (Equiv.addLeft a) = fun (x : G) => a + x
                                      @[simp]
                                      theorem Equiv.mulLeft_symm_apply {G : Type u_5} [Group G] (a : G) :
                                      (Equiv.symm (Equiv.mulLeft a)) = fun (x : G) => a⁻¹ * x

                                      Extra simp lemma that dsimp can use. simp will never use this.

                                      @[simp]
                                      theorem Equiv.addLeft_symm_apply {G : Type u_5} [AddGroup G] (a : G) :
                                      (Equiv.symm (Equiv.addLeft a)) = fun (x : G) => -a + x

                                      Extra simp lemma that dsimp can use. simp will never use this.

                                      @[simp]
                                      @[simp]
                                      theorem Group.mulLeft_bijective {G : Type u_5} [Group G] (a : G) :
                                      Function.Bijective fun (x : G) => a * x
                                      theorem AddGroup.addLeft_bijective {G : Type u_5} [AddGroup G] (a : G) :
                                      Function.Bijective fun (x : G) => a + x
                                      def Equiv.mulRight {G : Type u_5} [Group G] (a : G) :

                                      Right multiplication in a Group is a permutation of the underlying type.

                                      Equations
                                        Instances For
                                          def Equiv.addRight {G : Type u_5} [AddGroup G] (a : G) :

                                          Right addition in an AddGroup is a permutation of the underlying type.

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem Equiv.coe_mulRight {G : Type u_5} [Group G] (a : G) :
                                              (Equiv.mulRight a) = fun (x : G) => x * a
                                              @[simp]
                                              theorem Equiv.coe_addRight {G : Type u_5} [AddGroup G] (a : G) :
                                              (Equiv.addRight a) = fun (x : G) => x + a
                                              @[simp]
                                              @[simp]
                                              theorem Equiv.mulRight_symm_apply {G : Type u_5} [Group G] (a : G) :
                                              (Equiv.symm (Equiv.mulRight a)) = fun (x : G) => x * a⁻¹

                                              Extra simp lemma that dsimp can use. simp will never use this.

                                              @[simp]
                                              theorem Equiv.addRight_symm_apply {G : Type u_5} [AddGroup G] (a : G) :
                                              (Equiv.symm (Equiv.addRight a)) = fun (x : G) => x + -a

                                              Extra simp lemma that dsimp can use. simp will never use this.

                                              theorem Group.mulRight_bijective {G : Type u_5} [Group G] (a : G) :
                                              Function.Bijective fun (x : G) => x * a
                                              theorem AddGroup.addRight_bijective {G : Type u_5} [AddGroup G] (a : G) :
                                              Function.Bijective fun (x : G) => x + a
                                              def Equiv.divLeft {G : Type u_5} [Group G] (a : G) :
                                              G G

                                              A version of Equiv.mulLeft a b⁻¹ that is defeq to a / b.

                                              Equations
                                                Instances For
                                                  def Equiv.subLeft {G : Type u_5} [AddGroup G] (a : G) :
                                                  G G

                                                  A version of Equiv.addLeft a (-b) that is defeq to a - b.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Equiv.divLeft_symm_apply {G : Type u_5} [Group G] (a b : G) :
                                                      @[simp]
                                                      theorem Equiv.subLeft_symm_apply {G : Type u_5} [AddGroup G] (a b : G) :
                                                      @[simp]
                                                      theorem Equiv.divLeft_apply {G : Type u_5} [Group G] (a b : G) :
                                                      (Equiv.divLeft a) b = a / b
                                                      @[simp]
                                                      theorem Equiv.subLeft_apply {G : Type u_5} [AddGroup G] (a b : G) :
                                                      (Equiv.subLeft a) b = a - b
                                                      def Equiv.divRight {G : Type u_5} [Group G] (a : G) :
                                                      G G

                                                      A version of Equiv.mulRight a⁻¹ b that is defeq to b / a.

                                                      Equations
                                                        Instances For
                                                          def Equiv.subRight {G : Type u_5} [AddGroup G] (a : G) :
                                                          G G

                                                          A version of Equiv.addRight (-a) b that is defeq to b - a.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Equiv.subRight_apply {G : Type u_5} [AddGroup G] (a b : G) :
                                                              (Equiv.subRight a) b = b - a
                                                              @[simp]
                                                              theorem Equiv.divRight_apply {G : Type u_5} [Group G] (a b : G) :
                                                              (Equiv.divRight a) b = b / a
                                                              @[simp]
                                                              theorem Equiv.subRight_symm_apply {G : Type u_5} [AddGroup G] (a b : G) :
                                                              @[simp]
                                                              theorem Equiv.divRight_symm_apply {G : Type u_5} [Group G] (a b : G) :
                                                              def unitsEquivProdSubtype (α : Type u_2) [Monoid α] :
                                                              αˣ { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }

                                                              The αˣ type is equivalent to a subtype of α × α.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem unitsEquivProdSubtype_apply_coe (α : Type u_2) [Monoid α] (u : αˣ) :
                                                                  ((unitsEquivProdSubtype α) u) = (u, u⁻¹)
                                                                  @[simp]
                                                                  theorem val_unitsEquivProdSubtype_symm_apply (α : Type u_2) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }) :
                                                                  ((unitsEquivProdSubtype α).symm p) = (↑p).1
                                                                  @[simp]
                                                                  theorem val_inv_unitsEquivProdSubtype_symm_apply (α : Type u_2) [Monoid α] (p : { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }) :
                                                                  ((unitsEquivProdSubtype α).symm p)⁻¹ = (↑p).2
                                                                  def MulEquiv.inv (G : Type u_6) [DivisionCommMonoid G] :
                                                                  G ≃* G

                                                                  In a DivisionCommMonoid, Equiv.inv is a MulEquiv. There is a variant of this MulEquiv.inv' G : G ≃* Gᵐᵒᵖ for the non-commutative case.

                                                                  Equations
                                                                    Instances For

                                                                      When the AddGroup is commutative, Equiv.neg is an AddEquiv.

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem MulEquiv.inv_apply (G : Type u_6) [DivisionCommMonoid G] (a✝ : G) :
                                                                          (inv G) a✝ = a✝⁻¹
                                                                          @[simp]
                                                                          theorem AddEquiv.neg_apply (G : Type u_6) [SubtractionCommMonoid G] (a✝ : G) :
                                                                          (neg G) a✝ = -a✝
                                                                          @[simp]
                                                                          theorem MulEquiv.inv_symm (G : Type u_6) [DivisionCommMonoid G] :
                                                                          (inv G).symm = inv G
                                                                          @[simp]
                                                                          @[simp]
                                                                          theorem MulEquiv.isUnit_map {F : Type u_1} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [EquivLike F M N] [MulEquivClass F M N] (f : F) {x : M} :
                                                                          IsUnit (f x) IsUnit x
                                                                          @[simp]
                                                                          theorem AddEquiv.isAddUnit_map {F : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] [EquivLike F M N] [AddEquivClass F M N] (f : F) {x : M} :
                                                                          instance isLocalHom_equiv {F : Type u_1} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [EquivLike F M N] [MulEquivClass F M N] (f : F) :