proposition: Lemma dftE (v : 'rV[F]_n) : rVpoly (dft v) = \sum_(i in supp v) (v ``_ i *: \sum_(j < t) (a ``_ (inord j)) ^+ i *: 'X^j).
proof: Proof. rewrite /dft. under eq_bigr do rewrite scaler_sumr. rewrite exchange_big /= /rVpoly poly_def; apply eq_bigr => i _. under [in RHS]eq_bigr do rewrite scalerA. rewrite /fdcoor -scaler_suml; congr (_ *: _). rewrite insubT // => ni. rewrite mxE (@horner_coef_wide _ n); last by rewrite /rVpoly size_poly. rewrite -sum_supp; apply eq_bigr => j _. by rewrite coef_rVpoly_ord (_ : Sub _ _ = i) //; apply val_inj. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming