Geometric series: $\sum_{j=0}^{r-1}\omega_r^{jk} = 0$ for $1 \le k \le r-1$

Proved

ShorWiki.sum_omega_pow_mul_eq_zero

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-computingshor-algorithm

Let $r$ be a positive integer, $\omega_r = e^{2\pi i/r}$ , and $1 \le k \le r-1$ . Then

\sum_{j=0}^{r-1} \omega_r^{jk} = 0 .

This is the cancellation used to show that the uniform superposition of the eigenstates $|\psi_j\rangle$ collapses to the single basis state $|1\rangle$ .

Preamble

import Mathlib
import Definitions.Def_ShorWiki_Defs

open Matrix Kronecker

Formal statement

namespace ShorWiki

theorem sum_omega_pow_mul_eq_zero (r k : ℕ) (hk : 1 ≤ k) (hkr : k ≤ r - 1) :
    ∑ j ∈ Finset.range r, omega r ^ (j * k) = 0 := by sorry

end ShorWiki

Source

Wikipedia, "Shor's algorithm", revision oldid=1378862216, https://en.wikipedia.org/w/index.php?title=Shor%27s_algorithm&oldid=1378862216, section "Quantum phase estimation" (PDF p. 5)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Geometric series: ∑j=0r−1ωrjk=0\sum_{j=0}^{r-1}\omega_r^{jk} = 0∑j=0r−1​ωrjk​=0 for 1≤k≤r−11 \le k \le r-11≤k≤r−1

Geometric series: $\sum_{j=0}^{r-1}\omega_r^{jk} = 0$ for $1 \le k \le r-1$