proposition: Lemma dftK (v : 'rV[F]_n) : idft (dft (rVexp a n) n v) = v.
proof: Proof. apply/rowP => i; rewrite !mxE. rewrite /idft_coef. transitivity (n %:R^-1 * \sum_(k < n) \sum_(j' < n) v ``_ j' * a ^+ (j' * k) / a ^+ (i * k)). congr (_ * _). apply eq_bigr => k _. rewrite mxE /fdcoor horner_poly big_distrl /=; apply eq_bigr => j' _. rewrite insubT // => j'n. rewrite mxE inordK // -exprM mulnC; congr (v ``_ _ * _ * _); by apply val_inj. transitivity (n %:R^-1 * \sum_(j' < n) v ``_ j' * \sum_(k < n) a ^+ (j' * k) / a ^+ (i * k)). congr (_ * _); rewrite exchange_big /=. apply eq_bigr => i0 _. rewrite big_distrr /=; apply eq_bigr => j' _; by rewrite mulrA. rename i into j. rewrite (bigD1 j) //= (eq_bigr (fun=> 1)); last first. by move=> k _; rewrite divff // expf_neq0. rewrite sumr_const card_ord mulrDr mulrCA mulVr ?mulr1; last first. by rewrite unitfE natf_neq0. rewrite [X in _ + _ * X = _](_ : _ = 0) ?mulr0 ?addr0 //. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 // => i ij. apply/eqP. rewrite mulf_eq0; apply/orP; right. move: ij. rewrite neq_ltn => /orP[ij|ji]; last first. rewrite (eq_bigr (fun k : 'I_n => a ^+ (k * (i - j)))); last first. move=> k _. rewrite -exprB ?unitfE //; last first. by rewrite leq_mul // ltnW. by rewrite mulnBr 2!(mulnC k). rewrite (primitive_is_principal an) //. by rewrite subn_gt0 ji /= (leq_ltn_trans _ (ltn_ord i)) // leq_subr. rewrite (eq_bigr (fun k : 'I_n => a ^- ((j - i) * k))); last first. move=> k _. do 3 rewrite mulnC exprM. by rewrite exprB ?invf_div // ?unitfE ?expf_neq0 // ltnW. have abs : n.-primitive_root a^-1. apply/not_uroot_on_prim_root. - move=> k /andP[k0 kn]. move : an. rewrite /primitive_root_of_unity /= => /forallP/(_ (Ordinal (leq_ltn_trans (leq_pred _) kn))) /=. rewrite prednK // ltn_eqF // => /eqP. apply: contraFN => /eqP. rewrite exprVn => /(congr1 (fun x => x^-1))/eqP. by rewrite invrK invr1 unity_rootE. move/prim_expr_order : an => /(congr1 (fun x => x^-1)). by rewrite invr1 exprVn. have : 0 < j - i < n. by rewrite subn_gt0 ij /= (leq_ltn_trans _ (ltn_ord j)) // leq_subr. move/(primitive_is_principal abs) => {}abs. apply/eqP. rewrite -[in RHS]abs; apply/eq_bigr => k _. by rewrite exprVn mulnC. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming