Theorems · Definition · harmonic analysis

ZMod.dft

{N : ℕ} → [NeZero N] → {E : Type u_1} → [inst : AddCommGroup E] → [inst_1 : Module ℂ E] → (ZMod N → E) ≃ₗ[ℂ] ZMod N → E

The discrete Fourier transform on ℤ / N ℤ (with the counting measure), bundled as a linear equivalence. Denoted as 𝓕 within the ZMod namespace.

Defined in

Mathlib.Analysis.Fourier.ZMod

Cited by

25 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZeroAddCommGroupModule