Finite-index subgroup count for a finitely generated group (source code)

= Finite-index subgroup count for a finitely generated group
{title2=$\#\{H\leq G:[G:H]=n\}\leq n(n!)^d$}

If $G$ has $d$ generators, there are at most $(n!)^d$ <group homomorphisms> $G\to S_n$. Each <subgroup> of index $n$ is a point stabilizer in a transitive coset <group action>, so there are at most $n(n!)^d$ such subgroups. Consequently finitely many subgroups have index at most any fixed bound. Intersecting them gives a finite-index <characteristic subgroup>, useful in proving <residual finiteness of semidirect products>.