Saturated subgroups

Tags

subgroup, subgroups

ink

def AddSubgroup.Saturated {G : Type u_1} [inst : 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∈ H we have n = 0 or g ∈ H∈ H.

Equations

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

ink

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

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

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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