Documentation

Mathlib.GroupTheory.Subgroup.Saturated

Saturated subgroups #

Tags #

subgroup, subgroups

source
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
    Instances For
      source
      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
        Instances For
          source
          theorem Subgroup.saturated_iff_npow {G : Type u_1} [Group G] {H : Subgroup G} :
          H.Saturated ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
          source
          theorem AddSubgroup.saturated_iff_nsmul {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
          H.Saturated ↔ ∀ (n : ℕ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
          source
          theorem Subgroup.saturated_iff_zpow {G : Type u_1} [Group G] {H : Subgroup G} :
          H.Saturated ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H
          source
          theorem AddSubgroup.saturated_iff_zsmul {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
          H.Saturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
          source
          theorem AddSubgroup.ker_saturated {A₁ : Type u_1} {A₂ : Type u_2} [AddGroup A₁] [AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂) :
          f.ker.Saturated