Documentation

Mathlib.Algebra.Group.Submonoid.Units

Submonoid of units #

Given a submonoid S of a monoid M, we define the subgroup S.units as the units of S as a subgroup of . That is to say, S.units contains all members of S which have a two-sided inverse within S, as terms of type .

We also define, for subgroups S of , S.ofUnits, which is S considered as a submonoid of M. Submonoid.units and Subgroup.ofUnits form a Galois coinsertion.

We also make the equivalent additive definitions.

Implementation details #

There are a number of other constructions which are multiplicatively equivalent to S.units but which have a different type.

Definition Type
S.units Subgroup
Type u
IsUnit.submonoid S Submonoid S
S.units.ofUnits Submonoid M

All of these are distinct from S.leftInv, which is the submonoid of M which contains every member of M with a right inverse in S.

The additive units of S, packaged as an additive subgroup of AddUnits M.

Equations
Instances For
    def Submonoid.units {M : Type u_1} [Monoid M] (S : Submonoid M) :

    The units of S, packaged as a subgroup of .

    Equations
    Instances For

      A additive subgroup of additive units represented as a additive submonoid of M.

      Equations
      Instances For
        def Subgroup.ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) :

        A subgroup of units represented as a submonoid of M.

        Equations
        Instances For
          theorem AddSubmonoid.addUnits_mono {M : Type u_1} [AddMonoid M] :
          Monotone AddSubmonoid.addUnits
          theorem Submonoid.units_mono {M : Type u_1} [Monoid M] :
          Monotone Submonoid.units
          @[simp]
          theorem AddSubmonoid.ofAddUnits_addUnits_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
          S.addUnits.ofAddUnits S
          @[simp]
          theorem Submonoid.ofUnits_units_le {M : Type u_1} [Monoid M] (S : Submonoid M) :
          S.units.ofUnits S
          theorem AddSubgroup.ofAddUnits_mono {M : Type u_1} [AddMonoid M] :
          Monotone AddSubgroup.ofAddUnits
          theorem Subgroup.ofUnits_mono {M : Type u_1} [Monoid M] :
          Monotone Subgroup.ofUnits
          @[simp]
          theorem AddSubgroup.addUnits_ofAddUnits_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) :
          S.ofAddUnits.addUnits = S
          @[simp]
          theorem Subgroup.units_ofUnits_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) :
          S.ofUnits.units = S
          def ofAddUnits_addUnits_gci {M : Type u_1} [AddMonoid M] :
          GaloisCoinsertion AddSubgroup.ofAddUnits AddSubmonoid.addUnits

          A Galois coinsertion exists between the coercion from a additive subgroup of additive units to a additive submonoid and the reduction from a additive submonoid to its unit group.

          Equations
          Instances For
            def ofUnits_units_gci {M : Type u_1} [Monoid M] :
            GaloisCoinsertion Subgroup.ofUnits Submonoid.units

            A Galois coinsertion exists between the coercion from a subgroup of units to a submonoid and the reduction from a submonoid to its unit group.

            Equations
            Instances For
              theorem ofAddUnits_addUnits_gc {M : Type u_1} [AddMonoid M] :
              GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits
              theorem ofUnits_units_gc {M : Type u_1} [Monoid M] :
              GaloisConnection Subgroup.ofUnits Submonoid.units
              theorem ofAddUnits_le_iff_le_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (H : AddSubgroup (AddUnits M)) :
              H.ofAddUnits S H S.addUnits
              theorem ofUnits_le_iff_le_units {M : Type u_1} [Monoid M] (S : Submonoid M) (H : Subgroup Mˣ) :
              H.ofUnits S H S.units
              theorem AddSubmonoid.mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) :
              x S.addUnits x S (-x) S
              theorem Submonoid.mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) :
              x S.units x S x⁻¹ S
              theorem AddSubmonoid.mem_addUnits_of_val_mem_neg_val_mem {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h₁ : x S) (h₂ : (-x) S) :
              x S.addUnits
              theorem Submonoid.mem_units_of_val_mem_inv_val_mem {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h₁ : x S) (h₂ : x⁻¹ S) :
              x S.units
              theorem AddSubmonoid.val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x S.addUnits) :
              x S
              theorem Submonoid.val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x S.units) :
              x S
              theorem AddSubmonoid.neg_val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x S.addUnits) :
              (-x) S
              theorem Submonoid.inv_val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x S.units) :
              x⁻¹ S
              theorem AddSubmonoid.coe_neg_val_add_coe_val {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits S} :
              (-x) + x = 0
              theorem Submonoid.coe_inv_val_mul_coe_val {M : Type u_1} [Monoid M] (S : Submonoid M) {x : (↥S)ˣ} :
              x⁻¹ * x = 1
              theorem AddSubmonoid.coe_val_add_coe_neg_val {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits S} :
              x + (-x) = 0
              theorem Submonoid.coe_val_mul_coe_inv_val {M : Type u_1} [Monoid M] (S : Submonoid M) {x : (↥S)ˣ} :
              x * x⁻¹ = 1
              theorem AddSubmonoid.mk_neg_add_mk_eq_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x S.addUnits) :
              (AddUnits.coeHom M) (-x), + (AddUnits.coeHom M) x, = 0
              theorem Submonoid.mk_inv_mul_mk_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x S.units) :
              (Units.coeHom M) x⁻¹, * (Units.coeHom M) x, = 1
              theorem AddSubmonoid.mk_add_mk_neg_eq_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x S.addUnits) :
              (AddUnits.coeHom M) x, + (AddUnits.coeHom M) (-x), = 0
              theorem Submonoid.mk_mul_mk_inv_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x S.units) :
              (Units.coeHom M) x, * (Units.coeHom M) x⁻¹, = 1
              theorem AddSubmonoid.add_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} {y : AddUnits M} (h₁ : x S.addUnits) (h₂ : y S.addUnits) :
              x + y S.addUnits
              theorem Submonoid.mul_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} {y : Mˣ} (h₁ : x S.units) (h₂ : y S.units) :
              x * y S.units
              theorem AddSubmonoid.neg_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x S.addUnits) :
              -x S.addUnits
              theorem Submonoid.inv_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x S.units) :
              x⁻¹ S.units
              theorem AddSubmonoid.neg_mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} :
              -x S.addUnits x S.addUnits
              theorem Submonoid.inv_mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} :
              x⁻¹ S.units x S.units
              theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
              ∀ (x : S.addUnits), (fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, ) ((fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }) x) = (fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, ) ((fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }) x)
              theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits S) :
              { val := x, neg := (-x), val_neg := , neg_val := } (AddSubmonoid.comap (AddUnits.coeHom M) S) { val := x, neg := (-x), val_neg := , neg_val := } (-AddSubmonoid.comap (AddUnits.coeHom M) S)
              theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
              ∀ (x : AddUnits S), (fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }) ((fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, ) x) = (fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }) ((fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, ) x)
              def AddSubmonoid.addUnitsEquivAddUnitsType {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
              S.addUnits ≃+ AddUnits S

              The equivalence between the additive subgroup of additive units of S and the type of additive units of S.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                valS.addUnits, val (-AddSubmonoid.comap (AddUnits.coeHom M) S)
                theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                valS.addUnits, val (AddSubmonoid.comap (AddUnits.coeHom M) S)
                theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                ∀ (x x_1 : S.addUnits), { toFun := fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }, invFun := fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, , left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : S.addUnits) => match x with | val, h => { val := (AddUnits.coeHom M) val, , neg := (AddUnits.coeHom M) (-val), , val_neg := , neg_val := }, invFun := fun (x : AddUnits S) => { val := x, neg := (-x), val_neg := , neg_val := }, , left_inv := , right_inv := }.toFun (x + x_1)
                def Submonoid.unitsEquivUnitsType {M : Type u_1} [Monoid M] (S : Submonoid M) :
                S.units ≃* (↥S)ˣ

                The equivalence between the subgroup of units of S and the type of units of S.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem AddSubmonoid.addUnits_top {M : Type u_1} [AddMonoid M] :
                  .addUnits =
                  @[simp]
                  theorem Submonoid.units_top {M : Type u_1} [Monoid M] :
                  .units =
                  theorem AddSubmonoid.addUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (T : AddSubmonoid M) :
                  (S T).addUnits = S.addUnits T.addUnits
                  theorem Submonoid.units_inf {M : Type u_1} [Monoid M] (S : Submonoid M) (T : Submonoid M) :
                  (S T).units = S.units T.units
                  theorem AddSubmonoid.addUnits_sInf {M : Type u_1} [AddMonoid M] {s : Set (AddSubmonoid M)} :
                  (sInf s).addUnits = Ss, S.addUnits
                  theorem Submonoid.units_sInf {M : Type u_1} [Monoid M] {s : Set (Submonoid M)} :
                  (sInf s).units = Ss, S.units
                  theorem AddSubmonoid.addUnits_iInf {M : Type u_1} [AddMonoid M] {ι : Sort u_2} (f : ιAddSubmonoid M) :
                  (iInf f).addUnits = ⨅ (i : ι), (f i).addUnits
                  theorem Submonoid.units_iInf {M : Type u_1} [Monoid M] {ι : Sort u_2} (f : ιSubmonoid M) :
                  (iInf f).units = ⨅ (i : ι), (f i).units
                  theorem AddSubmonoid.addUnits_iInf₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ιSort u_3} (f : (i : ι) → κ iAddSubmonoid M) :
                  (⨅ (i : ι), ⨅ (j : κ i), f i j).addUnits = ⨅ (i : ι), ⨅ (j : κ i), (f i j).addUnits
                  theorem Submonoid.units_iInf₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ιSort u_3} (f : (i : ι) → κ iSubmonoid M) :
                  (⨅ (i : ι), ⨅ (j : κ i), f i j).units = ⨅ (i : ι), ⨅ (j : κ i), (f i j).units
                  @[simp]
                  theorem AddSubmonoid.addUnits_bot {M : Type u_1} [AddMonoid M] :
                  .addUnits =
                  @[simp]
                  theorem Submonoid.units_bot {M : Type u_1} [Monoid M] :
                  .units =
                  theorem AddSubmonoid.addUnits_surjective {M : Type u_1} [AddMonoid M] :
                  Function.Surjective AddSubmonoid.addUnits
                  theorem Submonoid.units_surjective {M : Type u_1} [Monoid M] :
                  Function.Surjective Submonoid.units
                  theorem AddSubmonoid.addUnits_left_inverse {M : Type u_1} [AddMonoid M] :
                  Function.LeftInverse AddSubmonoid.addUnits AddSubgroup.ofAddUnits
                  theorem Submonoid.units_left_inverse {M : Type u_1} [Monoid M] :
                  Function.LeftInverse Submonoid.units Subgroup.ofUnits
                  noncomputable def AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoid {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) :
                  S.addUnits ≃+ (IsAddUnit.addSubmonoid S)

                  The equivalence between the additive subgroup of additive units of S and the additive submonoid of additive unit elements of S.

                  Equations
                  • S.addUnitsEquivIsAddUnitAddSubmonoid = S.addUnitsEquivAddUnitsType.trans AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid
                  Instances For
                    noncomputable def Submonoid.unitsEquivIsUnitSubmonoid {M : Type u_1} [Monoid M] (S : Submonoid M) :
                    S.units ≃* (IsUnit.submonoid S)

                    The equivalence between the subgroup of units of S and the submonoid of unit elements of S.

                    Equations
                    • S.unitsEquivIsUnitSubmonoid = S.unitsEquivUnitsType.trans Submonoid.unitsTypeEquivIsUnitSubmonoid
                    Instances For
                      theorem AddSubgroup.mem_ofAddUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) :
                      x S.ofAddUnits yS, y = x
                      theorem Subgroup.mem_ofUnits_iff {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) :
                      x S.ofUnits yS, y = x
                      theorem AddSubgroup.mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {y : AddUnits M} (h₁ : y S) (h₂ : y = x) :
                      x S.ofAddUnits
                      theorem Subgroup.mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {y : Mˣ} (h₁ : y S) (h₂ : y = x) :
                      x S.ofUnits
                      theorem AddSubgroup.exists_mem_ofAddUnits_val_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x S.ofAddUnits) :
                      yS, y = x
                      theorem Subgroup.exists_mem_ofUnits_val_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x S.ofUnits) :
                      yS, y = x
                      theorem AddSubgroup.mem_of_mem_val_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {y : AddUnits M} (hy : y S.ofAddUnits) :
                      y S
                      theorem Subgroup.mem_of_mem_val_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {y : Mˣ} (hy : y S.ofUnits) :
                      y S
                      theorem AddSubgroup.isAddUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (hx : x S.ofAddUnits) :
                      theorem Subgroup.isUnit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (hx : x S.ofUnits) :
                      noncomputable def AddSubgroup.addUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x S.ofAddUnits) :

                      Given some x : M which is a member of the additive submonoid of additive unit elements corresponding to a subgroup of units, produce a unit of M whose coercion is equal to x.

                      Equations
                      Instances For
                        theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x S.ofAddUnits) :
                        theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x S.ofAddUnits) :
                        noncomputable def Subgroup.unit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x S.ofUnits) :

                        Given some x : M which is a member of the submonoid of unit elements corresponding to a subgroup of units, produce a unit of M whose coercion is equal to x. `

                        Equations
                        Instances For
                          theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_eq_of_val_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : AddUnits M} (h : x S.ofAddUnits) :
                          S.addUnit_of_mem_ofAddUnits h = x
                          theorem Subgroup.unit_of_mem_ofUnits_spec_eq_of_val_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : Mˣ} (h : x S.ofUnits) :
                          S.unit_of_mem_ofUnits h = x
                          theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_val_eq_of_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x S.ofAddUnits) :
                          (S.addUnit_of_mem_ofAddUnits h) = x
                          theorem Subgroup.unit_of_mem_ofUnits_spec_val_eq_of_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x S.ofUnits) :
                          (S.unit_of_mem_ofUnits h) = x
                          theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h : x S.ofAddUnits} :
                          S.addUnit_of_mem_ofAddUnits h S
                          theorem Subgroup.unit_of_mem_ofUnits_spec_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h : x S.ofUnits} :
                          S.unit_of_mem_ofUnits h S
                          theorem AddSubgroup.addUnit_eq_addUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x) (h₂ : x S.ofAddUnits) :
                          h₁.addUnit = S.addUnit_of_mem_ofAddUnits h₂
                          theorem Subgroup.unit_eq_unit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : x S.ofUnits) :
                          h₁.unit = S.unit_of_mem_ofUnits h₂
                          theorem AddSubgroup.addUnit_mem_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h₁ : IsAddUnit x} (h₂ : x S.ofAddUnits) :
                          h₁.addUnit S
                          theorem Subgroup.unit_mem_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h₁ : IsUnit x} (h₂ : x S.ofUnits) :
                          h₁.unit S
                          theorem AddSubgroup.mem_ofAddUnits_of_isAddUnit_of_addUnit_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h₁ : IsAddUnit x) (h₂ : h₁.addUnit S) :
                          x S.ofAddUnits
                          theorem Subgroup.mem_ofUnits_of_isUnit_of_unit_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : h₁.unit S) :
                          x S.ofUnits
                          theorem AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) :
                          x S.ofAddUnits ∃ (h : IsAddUnit x), h.addUnit S
                          theorem Subgroup.mem_ofUnits_iff_exists_isUnit {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) :
                          x S.ofUnits ∃ (h : IsUnit x), h.unit S
                          theorem AddSubgroup.ofAddUnitsEquivType.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : S.ofAddUnits) :
                          S.addUnit_of_mem_ofAddUnits S
                          theorem AddSubgroup.ofAddUnitsEquivType.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : S) :
                          aS.toAddSubmonoid, (AddUnits.coeHom M) a = x
                          theorem AddSubgroup.ofAddUnitsEquivType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) :
                          ∀ (x : S.ofAddUnits), (fun (x : S) => x, ) ((fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , ) x) = (fun (x : S) => x, ) ((fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , ) x)
                          noncomputable def AddSubgroup.ofAddUnitsEquivType {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) :
                          S.ofAddUnits ≃+ S

                          The equivalence between the coercion of an additive subgroup S of to an additive submonoid of M and the additive subgroup itself as a type.

                          Equations
                          • S.ofAddUnitsEquivType = { toFun := fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , , invFun := fun (x : S) => x, , left_inv := , right_inv := , map_add' := }
                          Instances For
                            theorem AddSubgroup.ofAddUnitsEquivType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) :
                            ∀ (x : S), (fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , ) ((fun (x : S) => x, ) x) = x
                            theorem AddSubgroup.ofAddUnitsEquivType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) :
                            ∀ (x x_1 : S.ofAddUnits), { toFun := fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , , invFun := fun (x : S) => x, , left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , , invFun := fun (x : S) => x, , left_inv := , right_inv := }.toFun x + { toFun := fun (x : S.ofAddUnits) => S.addUnit_of_mem_ofAddUnits , , invFun := fun (x : S) => x, , left_inv := , right_inv := }.toFun x_1
                            theorem AddSubgroup.ofAddUnitsEquivType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : S.ofAddUnits) :
                            x S.ofAddUnits
                            noncomputable def Subgroup.ofUnitsEquivType {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) :
                            S.ofUnits ≃* S

                            The equivalence between the coercion of a subgroup S of to a submonoid of M and the subgroup itself as a type.

                            Equations
                            • S.ofUnitsEquivType = { toFun := fun (x : S.ofUnits) => S.unit_of_mem_ofUnits , , invFun := fun (x : S) => x, , left_inv := , right_inv := , map_mul' := }
                            Instances For
                              @[simp]
                              theorem AddSubgroup.ofAddUnits_bot {M : Type u_1} [AddMonoid M] :
                              .ofAddUnits =
                              @[simp]
                              theorem Subgroup.ofUnits_bot {M : Type u_1} [Monoid M] :
                              .ofUnits =
                              theorem AddSubgroup.ofAddUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) :
                              (S T).ofAddUnits = S.ofAddUnits T.ofAddUnits
                              theorem Subgroup.ofUnits_inf {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) :
                              (S T).ofUnits = S.ofUnits T.ofUnits
                              theorem AddSubgroup.ofAddUnits_sSup {M : Type u_1} [AddMonoid M] (s : Set (AddSubgroup (AddUnits M))) :
                              (sSup s).ofAddUnits = Ss, S.ofAddUnits
                              theorem Subgroup.ofUnits_sSup {M : Type u_1} [Monoid M] (s : Set (Subgroup Mˣ)) :
                              (sSup s).ofUnits = Ss, S.ofUnits
                              theorem AddSubgroup.ofAddUnits_iSup {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {f : ιAddSubgroup (AddUnits M)} :
                              (iSup f).ofAddUnits = ⨆ (i : ι), (f i).ofAddUnits
                              theorem Subgroup.ofUnits_iSup {M : Type u_1} [Monoid M] {ι : Sort u_2} {f : ιSubgroup Mˣ} :
                              (iSup f).ofUnits = ⨆ (i : ι), (f i).ofUnits
                              theorem AddSubgroup.ofAddUnits_iSup₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ιSort u_3} (f : (i : ι) → κ iAddSubgroup (AddUnits M)) :
                              (⨆ (i : ι), ⨆ (j : κ i), f i j).ofAddUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofAddUnits
                              theorem Subgroup.ofUnits_iSup₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ιSort u_3} (f : (i : ι) → κ iSubgroup Mˣ) :
                              (⨆ (i : ι), ⨆ (j : κ i), f i j).ofUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofUnits
                              theorem AddSubgroup.ofAddUnits_injective {M : Type u_1} [AddMonoid M] :
                              Function.Injective AddSubgroup.ofAddUnits
                              theorem Subgroup.ofUnits_injective {M : Type u_1} [Monoid M] :
                              Function.Injective Subgroup.ofUnits
                              @[simp]
                              theorem AddSubgroup.ofAddUnits_sup_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) :
                              (S.ofAddUnits T.ofAddUnits).addUnits = S T
                              @[simp]
                              theorem Subgroup.ofUnits_sup_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) :
                              (S.ofUnits T.ofUnits).units = S T
                              @[simp]
                              theorem AddSubgroup.ofAddUnits_inf_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) :
                              (S.ofAddUnits T.ofAddUnits).addUnits = S T
                              @[simp]
                              theorem Subgroup.ofUnits_inf_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) :
                              (S.ofUnits T.ofUnits).units = S T
                              theorem AddSubgroup.ofAddUnits_right_inverse {M : Type u_1} [AddMonoid M] :
                              Function.RightInverse AddSubgroup.ofAddUnits AddSubmonoid.addUnits
                              theorem Subgroup.ofUnits_right_inverse {M : Type u_1} [Monoid M] :
                              Function.RightInverse Subgroup.ofUnits Submonoid.units
                              theorem AddSubgroup.ofAddUnits_strictMono {M : Type u_1} [AddMonoid M] :
                              StrictMono AddSubgroup.ofAddUnits
                              theorem Subgroup.ofUnits_strictMono {M : Type u_1} [Monoid M] :
                              StrictMono Subgroup.ofUnits
                              theorem Subgroup.ofUnits_le_ofUnits_iff {M : Type u_1} [Monoid M] {S : Subgroup Mˣ} {T : Subgroup Mˣ} :
                              S.ofUnits T.ofUnits S T
                              noncomputable def AddSubgroup.ofAddUnitsTopEquiv {M : Type u_1} [AddMonoid M] :
                              .ofAddUnits ≃+ AddUnits M

                              The equivalence between the additive subgroup of additive units of S and the additive submonoid of additive unit elements of S.

                              Equations
                              • AddSubgroup.ofAddUnitsTopEquiv = .ofAddUnitsEquivType.trans AddSubgroup.topEquiv
                              Instances For
                                noncomputable def Subgroup.ofUnitsTopEquiv {M : Type u_1} [Monoid M] :
                                .ofUnits ≃* Mˣ

                                The equivalence between the top subgroup of coerced to a submonoid M and the units of M.

                                Equations
                                • Subgroup.ofUnitsTopEquiv = .ofUnitsEquivType.trans Subgroup.topEquiv
                                Instances For
                                  theorem AddSubgroup.mem_addUnits_iff_val_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : AddUnits G) :
                                  x H.addUnits x H
                                  theorem Subgroup.mem_units_iff_val_mem {G : Type u_2} [Group G] (H : Subgroup G) (x : Gˣ) :
                                  x H.units x H
                                  theorem AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : G) :
                                  x H.ofAddUnits toAddUnits x H
                                  theorem Subgroup.mem_ofUnits_iff_toUnits_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : G) :
                                  x H.ofUnits toUnits x H
                                  @[simp]
                                  theorem AddSubgroup.mem_iff_toAddUnits_mem_addUnits {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : G) :
                                  toAddUnits x H.addUnits x H
                                  @[simp]
                                  theorem Subgroup.mem_iff_toUnits_mem_units {G : Type u_2} [Group G] (H : Subgroup G) (x : G) :
                                  toUnits x H.units x H
                                  @[simp]
                                  theorem AddSubgroup.val_mem_ofAddUnits_iff_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : AddUnits G) :
                                  x H.ofAddUnits x H
                                  @[simp]
                                  theorem Subgroup.val_mem_ofUnits_iff_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : Gˣ) :
                                  x H.ofUnits x H
                                  def AddSubgroup.addUnitsEquivSelf {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
                                  H.addUnits ≃+ H

                                  The equivalence between the greatest subgroup of additive units contained within T and T itself.

                                  Equations
                                  • H.addUnitsEquivSelf = H.addUnitsEquivAddUnitsType.trans toAddUnits.symm
                                  Instances For
                                    def Subgroup.unitsEquivSelf {G : Type u_2} [Group G] (H : Subgroup G) :
                                    H.units ≃* H

                                    The equivalence between the greatest subgroup of units contained within T and T itself.

                                    Equations
                                    • H.unitsEquivSelf = H.unitsEquivUnitsType.trans toUnits.symm
                                    Instances For