Steenrod powers on quaternionic projective space (source code)

= Steenrod powers on quaternionic projective space
{c}
{title2=$P^i(u^k)=\binom{2k}{i}u^{k+i(p-1)/2}$}

Choose the degree-four generator with pullback $u\mapsto x^2$ under the <complex inclusion into quaternionic projective space>. On infinite complex projective space, the <Cartan formula> gives $P^i(x^{2k})=\binom{2k}{i}x^{2k+i(p-1)}$. Injectivity of the infinite-space pullback proves the displayed formula for <quaternionic projective space>. Restriction to $\mathbb{HP}^n$ sets powers above $n$ to zero. Coefficients are reduced modulo the odd prime $p$; the exponent is an integer because $p-1$ is even.