Saturated subgroups

Tags

subgroup, subgroups

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

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

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

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

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

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

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

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

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

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

theorem AddSubgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [AddCommGroup A₁] [AddCommGroup A₂] [NoZeroSMulDivisors ℕ A₂] (f : A₁ →+ A₂) : AddSubgroup.Saturated (AddMonoidHom.ker f)