proposition: Lemma tdcoor_of_fdcoor i (v : 'rV[F]_n) : v``_i = n%:R^-1 * (rVpoly (dft (rVexp a n) n v)).[a ^- i].
proof: Proof. rewrite -[in LHS](dftK Hchar an v) mxE. rewrite /idft_coef; congr (_ * _); rewrite horner_poly. apply eq_bigr => j _. rewrite insubT // => jn. rewrite (_ : Sub _ _ = j); last by apply/val_inj. by rewrite -!exprVn exprM. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming