Strong completeness of finitely generated pro-p groups (source code)

= Strong completeness of finitely generated pro-p groups

Every abstract <subgroup> of finite index in a finitely generated <pro-p group> is open. <Fixed-generator commutator collection in nilpotent groups> makes the abstract <commutator subgroup> closed. The resulting abelian quotient is a quotient of a finite power of the <p-adic integers>, so its subgroup of $p$th powers is closed and of finite index. Thus the algebraic $G^p[G,G]$ is open and every abstract index-$p$ <subgroup> is open. An arbitrary finite quotient is a <finite p-group>; induction on its order, using a normal subgroup of index $p$ and the <Schreier lemma>, gives the assertion. The <normal core> reduces nonnormal finite-index <subgroups> to this case.