proposition: Lemma dft_syndromep (v : 'rV[F]_n) : rVpoly (dft (rVexp a n) t (twisted a v)) = syndromep (rVexp a n) v t.
proof: Proof. case/boolP : (a == 0) => [/eqP -> | a0]. apply/polyP => i. rewrite !coef_poly. case: ifPn => // it. rewrite insubT !mxE. rewrite /fdcoor !horner_poly. apply eq_bigr => j _. rewrite insubT // => jt. rewrite !mxE (_ : Sub _ _ = j); last by apply val_inj. rewrite (_ : Sub _ _ = Ordinal it) //=. rewrite inordK //; last by rewrite (leq_trans it) // ltnW. rewrite inordK; last by rewrite ltnS // (leq_trans it). rewrite !expr0n. set x := (i == _). case/boolP : (x) => //= Hx; first by rewrite expr1n mulr1. rewrite expr0n. set z := (_ == _). case/boolP : (z) => //= Hz; by [rewrite !mulr1 | rewrite !mulr0]. rewrite dftE /syndromep /fdcoor. transitivity (\sum_(i in supp v) (\sum_(j < t) (twisted a v) ``_ i * (rVexp a n) ``_ (inord j) ^+ i *: 'X^j)). rewrite supp_twisted //. apply eq_bigr => /= i _. rewrite scaler_sumr; apply eq_bigr => j _. by rewrite scalerA. rewrite exchange_big /= poly_def; apply eq_bigr => /= i _. rewrite horner_poly scaler_suml. transitivity (\sum_(i0 in 'I_n) ((twisted a v) ``_ i0 * (rVexp a n) ``_ (inord i) ^+ i0) *: 'X^i). apply/esym. rewrite (bigID (fun i => (twisted a v) ``_ i != 0)) /=. rewrite [X in _ + X = _](eq_bigr (fun => 0)); last first. move=> j. rewrite negbK => /eqP ->; by rewrite mul0r scale0r. rewrite big_const iter_addr0 addr0. apply eq_bigl => j; by rewrite mxE inE mulf_eq0 negb_or expf_neq0 // andbT. apply eq_bigr => /= j _. rewrite insubT // => jn. rewrite (_ : Sub _ _ = j); last by apply val_inj. rewrite !mxE inordK; last by rewrite (leq_trans (ltn_ord i)) // ltnW. rewrite inordK //; last by rewrite ltnS // (leq_trans (ltn_ord i)). by rewrite -exprM mulnC exprM -mulrA -exprS -exprM mulnC exprM. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft