Module

SigmaAllPrimes.lean

Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaAllPrimes

1 declaration indexed from sourceView source ↗

Module documentation

The set of all primes recovers ordinary faithfulness

Imports7

Imported by2

theorem

isSigmaAbFaithful_univ_iff

ProCGroups.FiniteStepSolvableQuotients.isSigmaAbFaithful_univ_iff

Documentation

Allowing all primes gives exactly ordinary abelianization-faithfulness.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem isSigmaAbFaithful_univ_iff {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    IsSigmaAbFaithful Set.univ G ↔ IsAbFaithful G