Prüfer rank bound for extensions (source code)

= Prüfer rank bound for extensions
{c}
{title2=$\operatorname{rk}_{\mathrm P}(G)\le\operatorname{rk}_{\mathrm P}(N)+\operatorname{rk}_{\mathrm P}(G/N)$}

For a <normal subgroup> $N$ with <Prüfer rank> $r$ and quotient of rank $s$, let $H=\langle h_1,\ldots,h_k\rangle\le G$. Choose at most $s$ elements $x_j\in H$ generating the image of $H$. Write $h_i=w_i(x_1,\ldots,x_s)n_i$ with $n_i\in N\cap H$. The finitely generated subgroup $\langle n_1,\ldots,n_k\rangle$ needs at most $r$ generators, so $H$ needs at most $r+s$. The full intersection $H\cap N$ need not be finitely generated.