fact: Definition dft (v : 'rV[F]_n) : 'rV[F]_t := \row_(k < t) v ^`_(a, inord k).
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming