Successive quotients of principal-unit groups (source code)

= Successive quotients of principal-unit groups
{title2=$U_r/U_{r+1}\cong(k,+),\quad U_r=1+\pi^r\mathcal O_K$}

For $r\geq1$, the map $1+\pi^r a\mapsto\bar a$ is a surjective group homomorphism to the additive <residue field> with kernel $U_{r+1}$. The extra product term is divisible by $\pi^{r+1}$. Thus each quotient has cardinality $|k|$, a useful count when splitting the <unit group> by roots of unity.