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

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.

Instances For

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

A subgroup of units represented as a submonoid of M.

Instances For

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

An additive subgroup of additive units represented as an additive submonoid of M.

Instances For

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

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

Monotone 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 ofUnits

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

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

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 an additive subgroup of additive units to an additive submonoid and the reduction from an additive submonoid to its unit group.

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 IsUnit.coe {M : Type u_1} [Monoid M] {S : Type u_2} [SetLike S M] [SubmonoidClass S M] {N : S} {a : ↥N} (ha : IsUnit a) :

theorem IsAddUnit.coe {M : Type u_1} [AddMonoid M] {S : Type u_2} [SetLike S M] [AddSubmonoidClass S M] {N : S} {a : ↥N} (ha : IsAddUnit a) :

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

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.

Instances For

@[simp]

theorem AddSubmonoid.val_addUnitsEquivAddUnitsType_symm_apply_coe {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits ↥S) :

↑↑(S.addUnitsEquivAddUnitsType.symm x) = ↑↑x

@[simp]

theorem Submonoid.val_unitsEquivUnitsType_apply_coe {M : Type u_1} [Monoid M] (S : Submonoid M) (x✝ : ↥S.units) :

↑↑(S.unitsEquivUnitsType x✝) = (Units.coeHom M) ↑x✝

@[simp]

theorem Submonoid.val_inv_unitsEquivUnitsType_apply_coe {M : Type u_1} [Monoid M] (S : Submonoid M) (x✝ : ↥S.units) :

↑↑(S.unitsEquivUnitsType x✝)⁻¹ = (Units.coeHom M) (↑x✝)⁻¹

@[simp]

theorem AddSubmonoid.val_addUnitsEquivAddUnitsType_apply_coe {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x✝ : ↥S.addUnits) :

↑↑(S.addUnitsEquivAddUnitsType x✝) = (AddUnits.coeHom M) ↑x✝

@[simp]

theorem AddSubmonoid.val_neg_addUnitsEquivAddUnitsType_apply_coe {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x✝ : ↥S.addUnits) :

↑↑(-S.addUnitsEquivAddUnitsType x✝) = (AddUnits.coeHom M) (-↑x✝)

@[simp]

theorem Submonoid.val_unitsEquivUnitsType_symm_apply_coe {M : Type u_1} [Monoid M] (S : Submonoid M) (x : (↥S)ˣ) :

↑↑(S.unitsEquivUnitsType.symm x) = ↑↑x

@[simp]

theorem AddSubmonoid.val_neg_addUnitsEquivAddUnitsType_symm_apply_coe {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits ↥S) :

↑(-↑(S.addUnitsEquivAddUnitsType.symm x)) = ↑↑(-x)

@[simp]

theorem Submonoid.val_inv_unitsEquivUnitsType_symm_apply_coe {M : Type u_1} [Monoid M] (S : Submonoid M) (x : (↥S)ˣ) :

↑(↑(S.unitsEquivUnitsType.symm x))⁻¹ = ↑↑x⁻¹

@[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 T : Submonoid M) :

(S ⊓ T).units = S.units ⊓ T.units

theorem AddSubmonoid.addUnits_inf {M : Type u_1} [AddMonoid M] (S 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 units

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

Function.Surjective addUnits

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

Function.LeftInverse units Subgroup.ofUnits

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

Function.LeftInverse 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.

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.

Instances For

instance Submonoid.instSubsingletonUnits {M : Type u_1} [Monoid M] [Subsingleton Mˣ] {S : Submonoid M} :

Subsingleton (↥S)ˣ

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.

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.

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.

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.

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 T : Subgroup Mˣ) :

(S ⊔ T).ofUnits = S.ofUnits ⊔ T.ofUnits

theorem AddSubgroup.ofAddUnits_inf {M : Type u_1} [AddMonoid M] (S 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 ofUnits

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

Function.Injective ofAddUnits

@[simp]

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

(S.ofUnits ⊔ T.ofUnits).units = S ⊔ T

@[simp]

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

(S.ofAddUnits ⊔ T.ofAddUnits).addUnits = S ⊔ T

@[simp]

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

(S.ofUnits ⊓ T.ofUnits).units = S ⊓ T

@[simp]

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

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

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

Function.RightInverse ofUnits Submonoid.units

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

Function.RightInverse ofAddUnits AddSubmonoid.addUnits

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

StrictMono ofUnits

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

StrictMono ofAddUnits

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

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.

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.

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.

Instances For