Module

PrimeSeparation.lean

Nyll.ProCGroups.ProC.PrimeSeparation

2 declarations indexed from sourceView source ↗

Module documentation

Separating distinct pro-prime group classes

Finite quotients of a group that is both pro-p and pro-q have trivial order at distinct primes. Applying this to the actual residual quotient shows that the maximal pro-q quotient of a pro-p group is trivial.

Imports4

Imported by2

theorem

subsingleton_of_hasOpenNormalBasisInClass_distinct_primes

L25 ↗

ProCGroups.ProC.subsingleton_of_hasOpenNormalBasisInClass_distinct_primes

Documentation

A Hausdorff group which is both pro-p and pro-q for distinct primes is trivial.

Source context 2 commands

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

namespace ProCGroups.ProC
universe u

Lean source · statement

theorem subsingleton_of_hasOpenNormalBasisInClass_distinct_primes
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
    (p q : ℕ) [Fact p.Prime] [Fact q.Prime] (hpq : p ≠ q)
    (hp : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (hq : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup q) G) : Subsingleton G

theorem

residualQuotient_subsingleton_of_distinct_primes

L46 ↗

ProCGroups.ProC.residualQuotient_subsingleton_of_distinct_primes