proposition: Lemma BCH_key_equation_old (y : 'rV[F]_n) : a ^+ n = 1 -> \sigma_(rVexp a n, y) * rVpoly (dft (rVexp a n) n y) = \BCHomega_(rVexp a n, y) * (1 - 'X^n).
proof: Proof. move=> an1. rewrite dftE big_distrr /=. under eq_bigr. move=> i ie. rewrite -scalerAr. rewrite (_ : \sigma_(rVexp a n, y) = \sigma_(rVexp a n, y, i) * (1 - ((rVexp a n) ``_ i) *: 'X)); last first. rewrite /errloc (bigD1 i) //= mulrC; congr (_ * _). apply eq_bigl => ij; by rewrite in_setD1 andbC. over. transitivity (\sum_(i in supp y) y ``_ i *: (\sigma_(rVexp a n, y, i) * (1 - a ^+ (i * n) *: 'X^n))). apply eq_bigr => /= i ie; congr (_ *: _). rewrite -mulrA; congr (_ * _). rewrite mulrDl mul1r mulNr big_distrr /=. rewrite [X in _ - X](eq_bigr (fun j : 'I_n => a ^+ (i * j.+1) *: 'X^j.+1)); last first. move=> j _. rewrite !mxE -scalerAr -scalerAl scalerA -exprM -exprD. by rewrite inord_val addnC -mulSn mulnC -exprS. rewrite big_ord_recl !mxE inord_val expr0 expr1n scale1r expr0. rewrite big_ord_recr /= opprD addrA. rewrite (_ : forall a b c d, b = c -> a + b - c - d = a - d) //. move=> a0 b c d -> //; by rewrite addrK. apply eq_bigr => j _; by rewrite mxE -exprM mulnC inordK // ltnS. rewrite /BCH_erreval [in RHS]big_distrl /=. apply eq_bigr => i ie. rewrite mxE -scalerAl mulr1; congr (_ *: (_ * _)). by rewrite mulnC exprM an1 expr1n scale1r. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2