# Saturated subgroups #

## Tags #

subgroup, subgroups

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

An additive subgroup H of G is saturated if for all n : ℕ and g : G with n•g ∈ H we have n = 0 or g ∈ H.

Equations
Instances For
def Subgroup.Saturated {G : Type u_1} [] (H : ) :

A subgroup H of G is saturated if for all n : ℕ and g : G with g^n ∈ H we have n = 0 or g ∈ H.

Equations
• H.Saturated = ∀ ⦃n : ⦄ ⦃g : G⦄, g ^ n Hn = 0 g H
Instances For
theorem AddSubgroup.saturated_iff_nsmul {G : Type u_1} [] {H : } :
H.Saturated ∀ (n : ) (g : G), n g Hn = 0 g H
theorem Subgroup.saturated_iff_npow {G : Type u_1} [] {H : } :
H.Saturated ∀ (n : ) (g : G), g ^ n Hn = 0 g H
theorem AddSubgroup.saturated_iff_zsmul {G : Type u_1} [] {H : } :
H.Saturated ∀ (n : ) (g : G), n g Hn = 0 g H
theorem Subgroup.saturated_iff_zpow {G : Type u_1} [] {H : } :
H.Saturated ∀ (n : ) (g : G), g ^ n Hn = 0 g H
theorem AddSubgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [] [] [] (f : A₁ →+ A₂) :
f.ker.Saturated