Lagrange idempotents for a root of unity over a commutative ring

Let $R$ be a commutative ring and $N$ a natural number, and write $m = N+1$. Assume the image of $m$ in $R$ is a unit; let $\zeta \in R$ satisfy $\zeta^{m} = 1$ together with the strong primitivity condition that $1 - \zeta^{j}$ is a unit of $R$ for every $j$ with $0 < j < m$; and let $\omega \in R$ satisfy $\omega^{m} = 1$. The conclusion is that there exists a family $e : \mathrm{Fin}(m) \to R$ which is a complete family of orthogonal idempotents in the sense of Mathlib's CompleteOrthogonalIdempotents, i.e. each $e_k$ is idempotent, $e_k e_l = 0$ for $k \ne l$, and $\sum_{k} e_k = 1$, and which diagonalises $\omega$ in the sense that $\omega \, e_k = \zeta^{k} e_k$ for every $k \in \mathrm{Fin}(m)$, where $k$ is read as a natural number in the exponent. No connectedness or local hypothesis on $R$ is imposed, and no uniqueness is asserted.

This is the Lagrange-resolvent decomposition: over a ring in which $N+1$ is invertible and $\zeta$ is a strong primitive $(N+1)$-st root of unity, $\operatorname{Spec} R$ splits into $N+1$ complementary open pieces on the $k$-th of which a given $(N+1)$-st root of unity $\omega$ equals $\zeta^{k}$. It is used in the theta-structure material, for instance to decompose a ring according to the values of an additive character and to diagonalise Schrödinger-type matrices, and is the base case of the corresponding statement for families of commuting roots of unity.