Documentation

Mathlib.GroupTheory.Subgroup.Saturated

Saturated subgroups #

Tags #

subgroup, subgroups

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

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
def Subgroup.Saturated {G : Type u_1} [inst : Group G] (H : Subgroup G) :

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
theorem AddSubgroup.saturated_iff_nsmul {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} :
AddSubgroup.Saturated H ∀ (n : ) (g : G), n g Hn = 0 g H
theorem Subgroup.saturated_iff_npow {G : Type u_1} [inst : Group G] {H : Subgroup G} :
Subgroup.Saturated H ∀ (n : ) (g : G), g ^ n Hn = 0 g H
theorem AddSubgroup.saturated_iff_zsmul {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} :
AddSubgroup.Saturated H ∀ (n : ) (g : G), n g Hn = 0 g H
theorem Subgroup.saturated_iff_zpow {G : Type u_1} [inst : Group G] {H : Subgroup G} :
Subgroup.Saturated H ∀ (n : ) (g : G), g ^ n Hn = 0 g H
theorem AddSubgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [inst : AddCommGroup A₁] [inst : AddCommGroup A₂] [inst : NoZeroSMulDivisors A₂] (f : A₁ →+ A₂) :