proposition: Lemma idft0 : idft (0 : 'rV[F]_n) = 0.
proof: Proof. rewrite /idft; apply/rowP => i; rewrite !mxE /idft_coef. apply/eqP; rewrite mulf_eq0; apply/orP; right. rewrite (eq_bigr (fun=> 0)); first by rewrite big_const iter_addr0. move=> j _; by rewrite mxE mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming