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

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

Equations

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

Instances For

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

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

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

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

Instances For

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

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

Equations

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

Instances For

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

Monotone Submonoid.units

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

Monotone AddSubmonoid.addUnits

@[simp]

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

S.units.ofUnits ≤ S

@[simp]

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

S.addUnits.ofAddUnits ≤ S

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

Monotone Subgroup.ofUnits

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

Monotone AddSubgroup.ofAddUnits

@[simp]

theorem Subgroup.units_ofUnits_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) :

S.ofUnits.units = S

@[simp]

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

S.ofAddUnits.addUnits = S

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 ⋯ ⋯ ⋯ ⋯

Instances For

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 ⋯ ⋯ ⋯ ⋯

Instances For

theorem ofUnits_units_gc {M : Type u_1} [Monoid M] :

GaloisConnection Subgroup.ofUnits Submonoid.units

theorem ofAddUnits_addUnits_gc {M : Type u_1} [AddMonoid M] :

GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.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 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 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_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) :

x ∈ S.addUnits ↔ ↑x ∈ S ∧ ↑(-x) ∈ 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 ∈ S.units

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.val_mem_of_mem_units {M : Type u_1} [Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) :

↑x ∈ S

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.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.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.coe_inv_val_mul_coe_val {M : Type u_1} [Monoid M] (S : Submonoid M) {x : (↥S)ˣ} :

↑↑x⁻¹ * ↑↑x = 1

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_val_mul_coe_inv_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.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_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_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.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.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.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.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 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} (h : 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.neg_mem_addUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M} :

-x ∈ S.addUnits ↔ x ∈ S.addUnits

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

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

@[simp]

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

⊤.units = ⊤

@[simp]

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

⊤.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_inf {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (T : AddSubmonoid M) :

(S ⊓ T).addUnits = S.addUnits ⊓ T.addUnits

theorem Submonoid.units_sInf {M : Type u_1} [Monoid M] {s : Set (Submonoid M)} :

(sInf s).units = ⨅ S ∈ s, S.units

theorem AddSubmonoid.addUnits_sInf {M : Type u_1} [AddMonoid M] {s : Set (AddSubmonoid M)} :

(sInf s).addUnits = ⨅ S ∈ s, S.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} (f : ι → AddSubmonoid M) :

(iInf f).addUnits = ⨅ (i : ι), (f i).addUnits

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

(⨅ (i : ι), ⨅ (j : κ i), f i j).units = ⨅ (i : ι), ⨅ (j : κ i), (f i j).units

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

(⨅ (i : ι), ⨅ (j : κ i), f i j).addUnits = ⨅ (i : ι), ⨅ (j : κ i), (f i j).addUnits

@[simp]

theorem Submonoid.units_bot {M : Type u_1} [Monoid M] :

⊥.units = ⊥

@[simp]

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

⊥.addUnits = ⊥

theorem Submonoid.units_surjective {M : Type u_1} [Monoid M] :

Function.Surjective Submonoid.units

theorem AddSubmonoid.addUnits_surjective {M : Type u_1} [AddMonoid M] :

Function.Surjective AddSubmonoid.addUnits

theorem Submonoid.units_left_inverse {M : Type u_1} [Monoid M] :

Function.LeftInverse Submonoid.units Subgroup.ofUnits

theorem AddSubmonoid.addUnits_left_inverse {M : Type u_1} [AddMonoid M] :

Function.LeftInverse AddSubmonoid.addUnits AddSubgroup.ofAddUnits

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

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

theorem Subgroup.mem_ofUnits_iff {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) (x : M) :

x ∈ S.ofUnits ↔ ∃ y ∈ S, ↑y = x

theorem AddSubgroup.mem_ofAddUnits_iff {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M) :

x ∈ S.ofAddUnits ↔ ∃ y ∈ S, ↑y = x

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.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.exists_mem_ofUnits_val_eq {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits) :

∃ y ∈ S, ↑y = x

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

∃ y ∈ S, ↑y = x

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.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.isUnit_of_mem_ofUnits {M : Type u_1} [Monoid M] (S : Subgroup Mˣ) {x : M} (hx : x ∈ S.ofUnits) :

theorem AddSubgroup.isAddUnit_of_mem_ofAddUnits {M : Type u_1} [AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (hx : 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

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

Instances For

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

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

Instances For

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_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_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_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_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_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_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_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_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.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.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_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_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.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

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 Mˣ 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

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 Mˣ 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

@[simp]

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

⊥.ofUnits = ⊥

@[simp]

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

⊥.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_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_sSup {M : Type u_1} [Monoid M] (s : Set (Subgroup Mˣ)) :

(sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits

theorem AddSubgroup.ofAddUnits_sSup {M : Type u_1} [AddMonoid M] (s : Set (AddSubgroup (AddUnits M))) :

(sSup s).ofAddUnits = ⨆ S ∈ s, S.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} {f : ι → AddSubgroup (AddUnits M)} :

(iSup f).ofAddUnits = ⨆ (i : ι), (f i).ofAddUnits

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

(⨆ (i : ι), ⨆ (j : κ i), f i j).ofUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofUnits

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

(⨆ (i : ι), ⨆ (j : κ i), f i j).ofAddUnits = ⨆ (i : ι), ⨆ (j : κ i), (f i j).ofAddUnits

theorem Subgroup.ofUnits_injective {M : Type u_1} [Monoid M] :

Function.Injective Subgroup.ofUnits

theorem AddSubgroup.ofAddUnits_injective {M : Type u_1} [AddMonoid M] :

Function.Injective AddSubgroup.ofAddUnits

@[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_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_inf_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

theorem Subgroup.ofUnits_right_inverse {M : Type u_1} [Monoid M] :

Function.RightInverse Subgroup.ofUnits Submonoid.units

theorem AddSubgroup.ofAddUnits_right_inverse {M : Type u_1} [AddMonoid M] :

Function.RightInverse AddSubgroup.ofAddUnits AddSubmonoid.addUnits

theorem Subgroup.ofUnits_strictMono {M : Type u_1} [Monoid M] :

StrictMono Subgroup.ofUnits

theorem AddSubgroup.ofAddUnits_strictMono {M : Type u_1} [AddMonoid M] :

StrictMono AddSubgroup.ofAddUnits

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 Subgroup.ofUnitsTopEquiv {M : Type u_1} [Monoid M] :

↥⊤.ofUnits ≃* Mˣ

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

Equations

Subgroup.ofUnitsTopEquiv = ⊤.ofUnitsEquivType.trans Subgroup.topEquiv

Instances For

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

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_addUnits_iff_val_mem {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (x : AddUnits G) :

x ∈ H.addUnits ↔ ↑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

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

@[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.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.val_mem_ofUnits_iff_mem {G : Type u_2} [Group G] (H : Subgroup Gˣ) (x : Gˣ) :

↑x ∈ H.ofUnits ↔ 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

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

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