If $\omega^{2^e}=-1$ then $\omega$ is a principal $2^{e+1}$ -th root of unity

Proved

IntMul.HvdH.sum_pow_eq_zero

by xuanji · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisinteger-multiplication

Let $R$ be any commutative ring and $\omega\in R$ with $\omega^{2^e}=-1$ . Then for every integer $j\ge0$ not divisible by $2^{e+1}$ ,

\sum_{k=0}^{2^{e+1}-1}\omega^{jk}=0 .

So $\omega$ is a principal $2^{e+1}$ -th root of unity in the sense of §2.4 of Harvey–van der Hoeven, even when $R$ has zero divisors. The main example is $R=\mathbb C[y]/(y^r+1)$ with $\omega=y^{2r/n}$ , $n\mid 2r$ .

Preamble

import Mathlib

Formal statement

namespace IntMul.HvdH
theorem sum_pow_eq_zero {R : Type*} [CommRing R] (e : ℕ) (ω : R) (hω : ω ^ (2 ^ e) = -1) (j : ℕ)
    (hj : ¬ 2 ^ (e + 1) ∣ j) : ∑ k ∈ Finset.range (2 ^ (e + 1)), ω ^ (j * k) = 0 := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Sections 2.4 and 3.1 (Lemma 2.3, (2.1), Lemma 3.2)

View graph

If ω2e=−1\omega^{2^e}=-1ω2e=−1 then ω\omegaω is a principal 2e+12^{e+1}2e+1-th root of unity

If $\omega^{2^e}=-1$ then $\omega$ is a principal $2^{e+1}$ -th root of unity