Frobenius substitution on cyclotomic power series (source code)

= Frobenius substitution on cyclotomic power series
{c}
{title2=$\varphi(f)(T)=f((1+T)^p-1)$}

= Frobenius substitutions on cyclotomic power series
{c}
{synonym}

On $R=\mathbb Z_p[[T]]$, this injective substitution reduces modulo $p$ to $f(T)\mapsto f(T^p)$. The ring is a free module of rank $p$ over $\varphi(R)$, with basis $1,(1+T),\ldots,(1+T)^{p-1}$. Prove this first modulo $p$, where the change of basis from $1,T,\ldots,T^{p-1}$ is triangular and invertible, and then lift coefficients successively modulo powers of $p$.