Documentation

Mathlib.GroupTheory.ResiduallyFinite

Residually Finite Groups #

In this file we define residually finite groups and prove some basic properties.

Main definitions #

source
class AddGroup.ResiduallyFinite (G : Type u_1) [AddGroup G] :
Prop

An additive group G is residually finite if the intersection of all finite index normal additive subgroups is trivial.

Instances
    source
    class Group.ResiduallyFinite (G : Type u_1) [Group G] :
    Prop

    A group G is residually finite if the intersection of all finite index normal subgroups is trivial.

    Instances
      source
      theorem Group.residuallyFinite_def {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup = ⊥
      source
      theorem AddGroup.residuallyFinite_def {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalAddSubgroup G), H.toAddSubgroup = ⊥
      source
      theorem Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
      source
      theorem AddGroup.residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) → g = 0
      source
      theorem Group.eq_one_iff_forall_finiteIndexNormalSubroup {G : Type u_1} [Group G] [ResiduallyFinite G] (g : G) (hg : ∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) :
      g = 1
      source
      theorem AddGroup.eq_zero_iff_forall_finiteIndexNormalSubroup {G : Type u_1} [AddGroup G] [ResiduallyFinite G] (g : G) (hg : ∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) :
      g = 0
      source
      theorem Group.residuallyFinite_iff_exists_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
      source
      theorem AddGroup.residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ (H : FiniteIndexNormalAddSubgroup G), g ∉ H
      source
      theorem Group.residuallyFinite_iff_forall_finiteIndex {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1
      source
      theorem Group.residuallyFinite_iff_exists_finiteIndex {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
      source
      instance Group.instResiduallyFiniteOfFinite {G : Type u_1} [Group G] [Finite G] :
      ResiduallyFinite G