Grover iterate

For an implicit natural number $N$ and an explicit index $w_0\in\{0,\dots,N-1\}$ (again, the type of $w_0$ forces $N\ge1$ implicitly), groverIterate w0 is defined as the composition of the continuous linear maps diffusion N and oracle w0, applied in the order "first oracle w0, then diffusion N" (i.e. for $z\in\mathbb{C}^N$, groverIterate w0$(z) =$ diffusion N$($oracle w0$(z))$). Unwinding both definitions: writing $z'=$oracle w0$(z)$, so $z'_{w_0}=-z_{w_0}$ and $z'_i=z_i$ for $i\neq w_0$, the result is $2\langle s,z'\rangle\, s - z'$ where $s=$uniformSuperposition N and $\langle s,z'\rangle=\tfrac{1}{\sqrt N}\sum_{i=0}^{N-1}z'_i=\tfrac{1}{\sqrt N}\Big(\sum_{i=0}^{N-1}z_i-2z_{w_0}\Big)$. No further hypotheses on $N$ or $w_0$ beyond their types are imposed, and the same junk-value conventions for $\sqrt{\cdot}$ and division apply as in the two component definitions.