proposition: Lemma dft0 (u : 'rV[F]_n) : (dft (rVexp a n) n u == 0) = (u == 0).
proof: Proof. apply/idP/idP => [/eqP|/eqP ->]. move/(congr1 (fun x => idft x)); by rewrite dftK idft0 => /eqP. apply/eqP/rowP => i; by rewrite !mxE fdcoor0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming