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 Mˣ. That is to say, S.units contains all members of S which have a two-sided inverse within S, as terms of type Mˣ.

We also define, for subgroups S of Mˣ, 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 Mˣ | | Sˣ | 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.

def AddSubmonoid.addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubgroup (AddUnits M)

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

Equations

• AddSubmonoid.addUnits S = { toAddSubmonoid := AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S, neg_mem' := ⋯ }

theorem AddSubmonoid.addUnits.proof_1 {M : Type u_1} [AddMonoid M] : AddMonoidHomClass (AddUnits M →+ M) (AddUnits M) M

theorem AddSubmonoid.addUnits.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ {x : AddUnits M}, x ∈ (AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S).carrier → -x ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) S) ∧ -x ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) S)

def Submonoid.units {M : Type u_1} [Monoid M] (S : Submonoid M) : Subgroup Mˣ

The units of S, packaged as a subgroup of Mˣ.

Equations

• Submonoid.units S = { toSubmonoid := Submonoid.comap (Units.coeHom M) S ⊓ (Submonoid.comap (Units.coeHom M) S)⁻¹, inv_mem' := ⋯ }

def AddSubgroup.ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : AddSubmonoid M

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

Equations

• AddSubgroup.ofAddUnits S = AddSubmonoid.map (AddUnits.coeHom M) S.toAddSubmonoid

theorem AddSubgroup.ofAddUnits.proof_1 {M : Type u_1} [AddMonoid M] : AddMonoidHomClass (AddUnits M →+ M) (AddUnits M) M

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

A subgroup of units represented as a submonoid of M.

Equations

• Subgroup.ofUnits S = Submonoid.map (Units.coeHom M) S.toSubmonoid

theorem AddSubmonoid.addUnits_mono {M : Type u_1} [AddMonoid M] : Monotone AddSubmonoid.addUnits

abbrev AddSubmonoid.addUnits_mono.match_1 {M : Type u_1} [AddMonoid M] : ∀ (x : AddSubmonoid M) (x_1 : AddUnits M) (motive : x_1 ∈ AddSubmonoid.addUnits x → Prop) (x_2 : x_1 ∈ AddSubmonoid.addUnits x), (∀ (h₁ : x_1 ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) x)) (h₂ : x_1 ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) x)), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

theorem Submonoid.units_mono {M : Type u_1} [Monoid M] : Monotone Submonoid.units

abbrev AddSubmonoid.ofAddUnits_addUnits_le.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : M) (motive : x ∈ AddSubgroup.ofAddUnits (AddSubmonoid.addUnits S) → Prop) (x_1 : x ∈ AddSubgroup.ofAddUnits (AddSubmonoid.addUnits S)), (∀ (w : AddUnits M) (hm : w ∈ ↑(AddSubmonoid.addUnits S).toAddSubmonoid) (he : (AddUnits.coeHom M) w = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

@[simp]

theorem AddSubmonoid.ofAddUnits_addUnits_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubgroup.ofAddUnits (AddSubmonoid.addUnits S) ≤ S

@[simp]

theorem Submonoid.ofUnits_units_le {M : Type u_1} [Monoid M] (S : Submonoid M) : Subgroup.ofUnits (Submonoid.units S) ≤ S

theorem AddSubgroup.ofAddUnits_mono {M : Type u_1} [AddMonoid M] : Monotone AddSubgroup.ofAddUnits

abbrev AddSubgroup.ofAddUnits_mono.match_1 {M : Type u_1} [AddMonoid M] : ∀ (x : AddSubgroup (AddUnits M)) (x_1 : M) (motive : x_1 ∈ AddSubgroup.ofAddUnits x → Prop) (x_2 : x_1 ∈ AddSubgroup.ofAddUnits x), (∀ (x_3 : AddUnits M) (hx : x_3 ∈ ↑x.toAddSubmonoid) (hy : (AddUnits.coeHom M) x_3 = x_1), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

theorem Subgroup.ofUnits_mono {M : Type u_1} [Monoid M] : Monotone Subgroup.ofUnits

abbrev AddSubgroup.addUnits_ofAddUnits_eq.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x : AddUnits M) (motive : x ∈ AddSubmonoid.addUnits (AddSubgroup.ofAddUnits S) → Prop) (x_1 : x ∈ AddSubmonoid.addUnits (AddSubgroup.ofAddUnits S)), (∀ (w : AddUnits M) (hm : w ∈ ↑S.toAddSubmonoid) (he : (AddUnits.coeHom M) w = (AddUnits.coeHom M) x) (right : x ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) (AddSubgroup.ofAddUnits S))), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

@[simp]

theorem AddSubgroup.addUnits_ofAddUnits_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : AddSubmonoid.addUnits (AddSubgroup.ofAddUnits S) = S

@[simp]

theorem Subgroup.units_ofUnits_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) : Submonoid.units (Subgroup.ofUnits S) = 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

• ofAddUnits_addUnits_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

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

• ofUnits_units_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯

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)) : AddSubgroup.ofAddUnits H ≤ S ↔ H ≤ AddSubmonoid.addUnits S

theorem ofUnits_le_iff_le_units {M : Type u_1} [Monoid M] (S : Submonoid M) (H : Subgroup Mˣ) : Subgroup.ofUnits H ≤ S ↔ H ≤ Submonoid.units S

theorem AddSubmonoid.mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) : x ∈ AddSubmonoid.addUnits S ↔ ↑x ∈ S ∧ ↑(-x) ∈ S

theorem Submonoid.mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) : x ∈ Submonoid.units S ↔ ↑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 ∈ AddSubmonoid.addUnits S

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 ∈ Submonoid.units S

theorem AddSubmonoid.val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ AddSubmonoid.addUnits S) : ↑x ∈ S

theorem Submonoid.val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ Submonoid.units S) : ↑x ∈ S

theorem AddSubmonoid.neg_val_mem_of_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ AddSubmonoid.addUnits S) : ↑(-x) ∈ S

theorem Submonoid.inv_val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ Submonoid.units S) : ↑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 ∈ AddSubmonoid.addUnits S) : { val := (AddUnits.coeHom M) (-x), property := ⋯ } + { val := (AddUnits.coeHom M) x, property := ⋯ } = 0

theorem Submonoid.mk_inv_mul_mk_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ Submonoid.units S) : { val := (Units.coeHom M) x⁻¹, property := ⋯ } * { val := (Units.coeHom M) x, property := ⋯ } = 1

theorem AddSubmonoid.mk_add_mk_neg_eq_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ AddSubmonoid.addUnits S) : { val := (AddUnits.coeHom M) x, property := ⋯ } + { val := (AddUnits.coeHom M) (-x), property := ⋯ } = 0

theorem Submonoid.mk_mul_mk_inv_eq_one {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ Submonoid.units S) : { val := (Units.coeHom M) x, property := ⋯ } * { val := (Units.coeHom M) x⁻¹, property := ⋯ } = 1

theorem AddSubmonoid.add_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} {y : AddUnits M} (h₁ : x ∈ AddSubmonoid.addUnits S) (h₂ : y ∈ AddSubmonoid.addUnits S) : x + y ∈ AddSubmonoid.addUnits S

theorem Submonoid.mul_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} {y : Mˣ} (h₁ : x ∈ Submonoid.units S) (h₂ : y ∈ Submonoid.units S) : x * y ∈ Submonoid.units S

theorem AddSubmonoid.neg_mem_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : x ∈ AddSubmonoid.addUnits S) : -x ∈ AddSubmonoid.addUnits S

theorem Submonoid.inv_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ Submonoid.units S) : x⁻¹ ∈ Submonoid.units S

theorem AddSubmonoid.neg_mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} : -x ∈ AddSubmonoid.addUnits S ↔ x ∈ AddSubmonoid.addUnits S

theorem Submonoid.inv_mem_units_iff {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} : x⁻¹ ∈ Submonoid.units S ↔ x ∈ Submonoid.units S

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ val ∈ AddSubmonoid.addUnits S, val ∈ ↑(AddSubmonoid.comap (AddUnits.coeHom M) S)

def AddSubmonoid.addUnitsEquivAddUnitsType {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ↥(AddSubmonoid.addUnits S) ≃+ 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.

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_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ val ∈ AddSubmonoid.addUnits S, val ∈ ↑(-AddSubmonoid.comap (AddUnits.coeHom M) S)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥(AddSubmonoid.addUnits S)), (fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }) ((fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) x) = (fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }) ((fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) x)

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥(AddSubmonoid.addUnits S)), { toFun := fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }, invFun := fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1)

abbrev AddSubmonoid.addUnitsEquivAddUnitsType.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (motive : ↥(AddSubmonoid.addUnits S) → Sort u_2) : (x : ↥(AddSubmonoid.addUnits S)) → ((val : AddUnits M) → (h : val ∈ AddSubmonoid.addUnits S) → motive { val := val, property := h }) → motive x

Equations

• AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S motive x h_1 = Subtype.casesOn x fun (val : AddUnits M) (property : val ∈ AddSubmonoid.addUnits S) => h_1 val property

theorem AddSubmonoid.addUnitsEquivAddUnitsType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : AddUnits ↥S), (fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) ((fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }) x) = (fun (x : ↥(AddSubmonoid.addUnits S)) => AddSubmonoid.addUnitsEquivAddUnitsType.match_1 S (fun (x : ↥(AddSubmonoid.addUnits S)) => AddUnits ↥S) x fun (val : AddUnits M) (h : val ∈ AddSubmonoid.addUnits S) => { val := { val := (AddUnits.coeHom M) val, property := ⋯ }, neg := { val := (AddUnits.coeHom M) (-val), property := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) ((fun (x : AddUnits ↥S) => { val := { val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, property := ⋯ }) x)

def Submonoid.unitsEquivUnitsType {M : Type u_1} [Monoid M] (S : Submonoid M) : ↥(Submonoid.units S) ≃* (↥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.

@[simp]

theorem AddSubmonoid.addUnits_top {M : Type u_1} [AddMonoid M] : AddSubmonoid.addUnits ⊤ = ⊤

@[simp]

theorem Submonoid.units_top {M : Type u_1} [Monoid M] : Submonoid.units ⊤ = ⊤

theorem AddSubmonoid.addUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (T : AddSubmonoid M) : AddSubmonoid.addUnits (S ⊓ T) = AddSubmonoid.addUnits S ⊓ AddSubmonoid.addUnits T

theorem Submonoid.units_inf {M : Type u_1} [Monoid M] (S : Submonoid M) (T : Submonoid M) : Submonoid.units (S ⊓ T) = Submonoid.units S ⊓ Submonoid.units T

theorem AddSubmonoid.addUnits_sInf {M : Type u_1} [AddMonoid M] {s : Set (AddSubmonoid M)} : AddSubmonoid.addUnits (sInf s) = ⨅ S ∈ s, AddSubmonoid.addUnits S

theorem Submonoid.units_sInf {M : Type u_1} [Monoid M] {s : Set (Submonoid M)} : Submonoid.units (sInf s) = ⨅ S ∈ s, Submonoid.units S

theorem AddSubmonoid.addUnits_iInf {M : Type u_1} [AddMonoid M] {ι : Sort u_2} (f : ι → AddSubmonoid M) : AddSubmonoid.addUnits (iInf f) = ⨅ (i : ι), AddSubmonoid.addUnits (f i)

theorem Submonoid.units_iInf {M : Type u_1} [Monoid M] {ι : Sort u_2} (f : ι → Submonoid M) : Submonoid.units (iInf f) = ⨅ (i : ι), Submonoid.units (f i)

theorem AddSubmonoid.addUnits_iInf₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubmonoid M) : AddSubmonoid.addUnits (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), AddSubmonoid.addUnits (f i j)

theorem Submonoid.units_iInf₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Submonoid M) : Submonoid.units (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), Submonoid.units (f i j)

@[simp]

theorem AddSubmonoid.addUnits_bot {M : Type u_1} [AddMonoid M] : AddSubmonoid.addUnits ⊥ = ⊥

@[simp]

theorem Submonoid.units_bot {M : Type u_1} [Monoid M] : Submonoid.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) : ↥(AddSubmonoid.addUnits S) ≃+ ↥(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

• AddSubmonoid.addUnitsEquivIsAddUnitAddSubmonoid S = AddEquiv.trans (AddSubmonoid.addUnitsEquivAddUnitsType S) AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid

noncomputable def Submonoid.unitsEquivIsUnitSubmonoid {M : Type u_1} [Monoid M] (S : Submonoid M) : ↥(Submonoid.units S) ≃* ↥(IsUnit.submonoid ↥S)

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

Equations

• Submonoid.unitsEquivIsUnitSubmonoid S = MulEquiv.trans (Submonoid.unitsEquivUnitsType S) Submonoid.unitsTypeEquivIsUnitSubmonoid

theorem AddSubgroup.mem_ofAddUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) : x ∈ AddSubgroup.ofAddUnits S ↔ ∃ y ∈ S, ↑y = x

theorem Subgroup.mem_ofUnits_iff {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) : x ∈ Subgroup.ofUnits S ↔ ∃ y ∈ S, ↑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 ∈ AddSubgroup.ofAddUnits S

theorem Subgroup.mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {y : Mˣ} (h₁ : y ∈ S) (h₂ : ↑y = x) : x ∈ Subgroup.ofUnits S

theorem AddSubgroup.exists_mem_ofAddUnits_val_eq {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ AddSubgroup.ofAddUnits S) : ∃ y ∈ S, ↑y = x

theorem Subgroup.exists_mem_ofUnits_val_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ Subgroup.ofUnits S) : ∃ y ∈ S, ↑y = x

theorem AddSubgroup.mem_of_mem_val_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {y : AddUnits M} (hy : ↑y ∈ AddSubgroup.ofAddUnits S) : y ∈ S

abbrev AddSubgroup.mem_of_mem_val_ofAddUnits.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {y : AddUnits M} (motive : ↑y ∈ AddSubgroup.ofAddUnits S → Prop) : ∀ (hy : ↑y ∈ AddSubgroup.ofAddUnits S), (∀ (w : AddUnits M) (hm : w ∈ ↑S.toAddSubmonoid) (he : (AddUnits.coeHom M) w = ↑y), motive ⋯) → motive hy

Equations

• ⋯ = ⋯

theorem Subgroup.mem_of_mem_val_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {y : Mˣ} (hy : ↑y ∈ Subgroup.ofUnits S) : y ∈ S

theorem AddSubgroup.isAddUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (hx : x ∈ AddSubgroup.ofAddUnits S) : IsAddUnit x

abbrev AddSubgroup.isAddUnit_of_mem_ofAddUnits.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (motive : x ∈ AddSubgroup.ofAddUnits S → Prop) : ∀ (hx : x ∈ AddSubgroup.ofAddUnits S), (∀ (w : AddUnits M) (left : w ∈ ↑S.toAddSubmonoid) (h : (AddUnits.coeHom M) w = x), motive ⋯) → motive hx

Equations

• ⋯ = ⋯

theorem Subgroup.isUnit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (hx : x ∈ Subgroup.ofUnits S) : IsUnit x

theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ AddSubgroup.ofAddUnits S) : ↑(-Classical.choose h) = ↑(-Classical.choose h)

noncomputable def AddSubgroup.addUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ AddSubgroup.ofAddUnits S) : AddUnits M

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

• AddSubgroup.addUnit_of_mem_ofAddUnits S h = AddUnits.copy (Classical.choose h) x ⋯ ↑(-Classical.choose h) ⋯

theorem AddSubgroup.addUnit_of_mem_ofAddUnits.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ AddSubgroup.ofAddUnits S) : x = (AddUnits.coeHom M) (Classical.choose h)

noncomputable def Subgroup.unit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ Subgroup.ofUnits S) : Mˣ

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

• Subgroup.unit_of_mem_ofUnits S h = Units.copy (Classical.choose h) x ⋯ ↑(Classical.choose h)⁻¹ ⋯

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 ∈ AddSubgroup.ofAddUnits S) : AddSubgroup.addUnit_of_mem_ofAddUnits S 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 ∈ Subgroup.ofUnits S) : Subgroup.unit_of_mem_ofUnits S 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 ∈ AddSubgroup.ofAddUnits S) : ↑(AddSubgroup.addUnit_of_mem_ofAddUnits S 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 ∈ Subgroup.ofUnits S) : ↑(Subgroup.unit_of_mem_ofUnits S h) = x

theorem AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} {h : x ∈ AddSubgroup.ofAddUnits S} : AddSubgroup.addUnit_of_mem_ofAddUnits S h ∈ S

theorem Subgroup.unit_of_mem_ofUnits_spec_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h : x ∈ Subgroup.ofUnits S} : Subgroup.unit_of_mem_ofUnits S 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 ∈ AddSubgroup.ofAddUnits S) : IsAddUnit.addUnit h₁ = AddSubgroup.addUnit_of_mem_ofAddUnits S 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 ∈ Subgroup.ofUnits S) : IsUnit.unit h₁ = Subgroup.unit_of_mem_ofUnits S 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 ∈ AddSubgroup.ofAddUnits S) : IsAddUnit.addUnit h₁ ∈ S

theorem Subgroup.unit_mem_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} {h₁ : IsUnit x} (h₂ : x ∈ Subgroup.ofUnits S) : IsUnit.unit h₁ ∈ 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₂ : IsAddUnit.addUnit h₁ ∈ S) : x ∈ AddSubgroup.ofAddUnits S

theorem Subgroup.mem_ofUnits_of_isUnit_of_unit_mem {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : IsUnit.unit h₁ ∈ S) : x ∈ Subgroup.ofUnits S

abbrev AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) (motive : (∃ (h : IsAddUnit x), IsAddUnit.addUnit h ∈ S) → Prop) : ∀ (x_1 : ∃ (h : IsAddUnit x), IsAddUnit.addUnit h ∈ S), (∀ (hm : IsAddUnit x) (he : IsAddUnit.addUnit hm ∈ S), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) : x ∈ AddSubgroup.ofAddUnits S ↔ ∃ (h : IsAddUnit x), IsAddUnit.addUnit h ∈ S

theorem Subgroup.mem_ofUnits_iff_exists_isUnit {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) : x ∈ Subgroup.ofUnits S ↔ ∃ (h : IsUnit x), IsUnit.unit h ∈ S

theorem AddSubgroup.ofAddUnitsEquivType.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x : ↥(AddSubgroup.ofAddUnits S)), (fun (x : ↥S) => { val := ↑↑x, property := ⋯ }) ((fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }) x) = (fun (x : ↥S) => { val := ↑↑x, property := ⋯ }) ((fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }) x)

theorem AddSubgroup.ofAddUnitsEquivType.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : ↥(AddSubgroup.ofAddUnits S)) : AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯ ∈ S

theorem AddSubgroup.ofAddUnitsEquivType.proof_6 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x x_1 : ↥(AddSubgroup.ofAddUnits S)), { toFun := fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }, invFun := fun (x : ↥S) => { val := ↑↑x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }, invFun := fun (x : ↥S) => { val := ↑↑x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }, invFun := fun (x : ↥S) => { val := ↑↑x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun x_1

noncomputable def AddSubgroup.ofAddUnitsEquivType {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ↥(AddSubgroup.ofAddUnits S) ≃+ ↥S

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

Equations

• One or more equations did not get rendered due to their size.

theorem AddSubgroup.ofAddUnitsEquivType.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) : ∀ (x : ↥S), (fun (x : ↥(AddSubgroup.ofAddUnits S)) => { val := AddSubgroup.addUnit_of_mem_ofAddUnits S ⋯, property := ⋯ }) ((fun (x : ↥S) => { val := ↑↑x, property := ⋯ }) x) = x

theorem AddSubgroup.ofAddUnitsEquivType.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : ↥S) : ∃ a ∈ ↑S.toAddSubmonoid, (AddUnits.coeHom M) a = ↑↑x

theorem AddSubgroup.ofAddUnitsEquivType.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : ↥(AddSubgroup.ofAddUnits S)) : ↑x ∈ AddSubgroup.ofAddUnits S

noncomputable def Subgroup.ofUnitsEquivType {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) : ↥(Subgroup.ofUnits S) ≃* ↥S

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubgroup.ofAddUnits_bot {M : Type u_1} [AddMonoid M] : AddSubgroup.ofAddUnits ⊥ = ⊥

@[simp]

theorem Subgroup.ofUnits_bot {M : Type u_1} [Monoid M] : Subgroup.ofUnits ⊥ = ⊥

theorem AddSubgroup.ofAddUnits_inf {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) : AddSubgroup.ofAddUnits (S ⊔ T) = AddSubgroup.ofAddUnits S ⊔ AddSubgroup.ofAddUnits T

theorem Subgroup.ofUnits_inf {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : Subgroup.ofUnits (S ⊔ T) = Subgroup.ofUnits S ⊔ Subgroup.ofUnits T

theorem AddSubgroup.ofAddUnits_sSup {M : Type u_1} [AddMonoid M] (s : Set (AddSubgroup (AddUnits M))) : AddSubgroup.ofAddUnits (sSup s) = ⨆ S ∈ s, AddSubgroup.ofAddUnits S

theorem Subgroup.ofUnits_sSup {M : Type u_1} [Monoid M] (s : Set (Subgroup Mˣ)) : Subgroup.ofUnits (sSup s) = ⨆ S ∈ s, Subgroup.ofUnits S

theorem AddSubgroup.ofAddUnits_iSup {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {f : ι → AddSubgroup (AddUnits M)} : AddSubgroup.ofAddUnits (iSup f) = ⨆ (i : ι), AddSubgroup.ofAddUnits (f i)

theorem Subgroup.ofUnits_iSup {M : Type u_1} [Monoid M] {ι : Sort u_2} {f : ι → Subgroup Mˣ} : Subgroup.ofUnits (iSup f) = ⨆ (i : ι), Subgroup.ofUnits (f i)

theorem AddSubgroup.ofAddUnits_iSup₂ {M : Type u_1} [AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubgroup (AddUnits M)) : AddSubgroup.ofAddUnits (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), AddSubgroup.ofAddUnits (f i j)

theorem Subgroup.ofUnits_iSup₂ {M : Type u_1} [Monoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → Subgroup Mˣ) : Subgroup.ofUnits (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), Subgroup.ofUnits (f i j)

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)) : AddSubmonoid.addUnits (AddSubgroup.ofAddUnits S ⊔ AddSubgroup.ofAddUnits T) = S ⊔ T

@[simp]

theorem Subgroup.ofUnits_sup_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : Submonoid.units (Subgroup.ofUnits S ⊔ Subgroup.ofUnits T) = S ⊔ T

@[simp]

theorem AddSubgroup.ofAddUnits_inf_addUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (T : AddSubgroup (AddUnits M)) : AddSubmonoid.addUnits (AddSubgroup.ofAddUnits S ⊓ AddSubgroup.ofAddUnits T) = S ⊓ T

@[simp]

theorem Subgroup.ofUnits_inf_units {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (T : Subgroup Mˣ) : Submonoid.units (Subgroup.ofUnits S ⊓ Subgroup.ofUnits T) = 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ˣ} : Subgroup.ofUnits S ≤ Subgroup.ofUnits T ↔ S ≤ T

noncomputable def AddSubgroup.ofAddUnitsTopEquiv {M : Type u_1} [AddMonoid M] : ↥(AddSubgroup.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 = AddEquiv.trans (AddSubgroup.ofAddUnitsEquivType ⊤) AddSubgroup.topEquiv

noncomputable def Subgroup.ofUnitsTopEquiv {M : Type u_1} [Monoid M] : ↥(Subgroup.ofUnits ⊤) ≃* Mˣ

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

Equations

• Subgroup.ofUnitsTopEquiv = MulEquiv.trans (Subgroup.ofUnitsEquivType ⊤) Subgroup.topEquiv

theorem AddSubgroup.mem_addUnits_iff_val_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : AddUnits G) : x ∈ AddSubmonoid.addUnits H.toAddSubmonoid ↔ ↑x ∈ H

theorem Subgroup.mem_units_iff_val_mem {G : Type u_2} [Group G] (H : Subgroup G) (x : Gˣ) : x ∈ Submonoid.units H.toSubmonoid ↔ ↑x ∈ H

theorem AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : G) : x ∈ AddSubgroup.ofAddUnits H ↔ toAddUnits x ∈ H

theorem Subgroup.mem_ofUnits_iff_toUnits_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : G) : x ∈ Subgroup.ofUnits H ↔ toUnits x ∈ H

@[simp]

theorem AddSubgroup.mem_iff_toAddUnits_mem_addUnits {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : G) : toAddUnits x ∈ AddSubmonoid.addUnits H.toAddSubmonoid ↔ x ∈ H

@[simp]

theorem Subgroup.mem_iff_toUnits_mem_units {G : Type u_2} [Group G] (H : Subgroup G) (x : G) : toUnits x ∈ Submonoid.units H.toSubmonoid ↔ x ∈ H

@[simp]

theorem AddSubgroup.val_mem_ofAddUnits_iff_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup (AddUnits G)) (x : AddUnits G) : ↑x ∈ AddSubgroup.ofAddUnits H ↔ x ∈ H

@[simp]

theorem Subgroup.val_mem_ofUnits_iff_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : Gˣ) : ↑x ∈ Subgroup.ofUnits H ↔ x ∈ H

def AddSubgroup.addUnitsEquivSelf {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : ↥(AddSubmonoid.addUnits H.toAddSubmonoid) ≃+ ↥H

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

Equations

• AddSubgroup.addUnitsEquivSelf H = AddEquiv.trans (AddSubmonoid.addUnitsEquivAddUnitsType H.toAddSubmonoid) (AddEquiv.symm toAddUnits)

def Subgroup.unitsEquivSelf {G : Type u_2} [Group G] (H : Subgroup G) : ↥(Submonoid.units H.toSubmonoid) ≃* ↥H

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

Equations

• Subgroup.unitsEquivSelf H = MulEquiv.trans (Submonoid.unitsEquivUnitsType H.toSubmonoid) (MulEquiv.symm toUnits)