Saturated subgroups

Tags

subgroup, subgroups

def Submonoid.PowSaturated {G : Type u_1} [Monoid G] (H : Submonoid G) : Prop

A submonoid H of G is saturated if for all n : ℕ and g : G with g^n ∈ H we have n = 0 or g ∈ H. We use the name PowSaturated to distinguish from Submonoid.MulSaturated.

Equations

• H.PowSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H

def AddSubmonoid.NSMulSaturated {G : Type u_1} [AddMonoid G] (H : AddSubmonoid G) : Prop

An additive submonoid H of G is saturated if for all n : ℕ and g : G with n•g ∈ H we have n = 0 or g ∈ H. We use the name NSMulSaturated to distinguish from Submonoid.MulSaturated.

Equations

• H.NSMulSaturated = ∀ ⦃n : ℕ⦄ ⦃g : G⦄, n • g ∈ H → n = 0 ∨ g ∈ H

theorem Submonoid.powSaturated_iff_npow {G : Type u_1} [Monoid G] {H : Submonoid G} : H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem AddSubmonoid.nsmulSaturated_iff_nsmul {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} : H.NSMulSaturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

@[deprecated Submonoid.PowSaturated (since := "2026-03-03")]

def Subgroup.Saturated {G : Type u_1} [Monoid G] (H : Submonoid G) : Prop

Alias of Submonoid.PowSaturated.

---

A submonoid H of G is saturated if for all n : ℕ and g : G with g^n ∈ H we have n = 0 or g ∈ H. We use the name PowSaturated to distinguish from Submonoid.MulSaturated.

Equations

• @Subgroup.Saturated = @Submonoid.PowSaturated

@[deprecated AddSubmonoid.NSMulSaturated (since := "2026-03-03")]

def AddSubgroup.Saturated {G : Type u_1} [AddMonoid G] (H : AddSubmonoid G) : Prop

Alias of AddSubmonoid.NSMulSaturated.

---

An additive submonoid H of G is saturated if for all n : ℕ and g : G with n•g ∈ H we have n = 0 or g ∈ H. We use the name NSMulSaturated to distinguish from Submonoid.MulSaturated.

Equations

• @AddSubgroup.Saturated = @AddSubmonoid.NSMulSaturated

@[deprecated Submonoid.powSaturated_iff_npow (since := "2026-03-03")]

theorem Subgroup.saturated_iff_npow {G : Type u_1} [Monoid G] {H : Submonoid G} : H.PowSaturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

Alias of Submonoid.powSaturated_iff_npow.

@[deprecated AddSubmonoid.nsmulSaturated_iff_nsmul (since := "2026-03-03")]

theorem AddSubgroup.saturated_iff_nsmul {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} : H.NSMulSaturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

Alias of AddSubmonoid.nsmulSaturated_iff_nsmul.

theorem Subgroup.saturated_iff_zpow {G : Type u_1} [Group G] {H : Subgroup G} : H.PowSaturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H

theorem AddSubgroup.saturated_iff_zsmul {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.NSMulSaturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H

theorem AddSubmonoid.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [AddGroup A₁] [AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂) : f.ker.NSMulSaturated

@[deprecated AddSubmonoid.ker_saturated (since := "2026-03-03")]

theorem AddSubgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [AddGroup A₁] [AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂) : f.ker.NSMulSaturated

Alias of AddSubmonoid.ker_saturated.