noncomputable def ProjectionTheory.modProjection (N p : ℕ) (f : Fin N → ℂ) (a : ZMod p) : ℂ

Projection $\pi_p f : \mathbb{Z}_p \to \mathbb{C}$ onto the subspace indexed by $\mathbb{Z}_p$: at residue $a$ it sums $f(n)$ over those $n \in [N]$ with $n \equiv a \pmod p$. A companion definition expressing the dictionary $\widehat{\pi_V f}(\xi) = \hat f(\xi)$ for $V = \mathbb{Z}_p$.