fact: Definition idft (f : 'rV[F]_n) : 'rV[F]_n := \row_(i < n) idft_coef f i.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming