proposition: Lemma BCH_key_equation y : \sigma_(rVexp a n, F2_to_GF2 m y) * \BCHsynp_(rVexp a n, y, t) = \BCHomega_(rVexp a n, twisted a (F2_to_GF2 m y)) + BCH_mod (F2_to_GF2 m y) * 'X^t.*2.
proof: Proof. move: (@GRS_key_equation F n (F2_to_GF2 m y) (rVexp a n) (rVexp a n) t.*2) => H0. rewrite BCH_syndromep_is_GRS_syndromep // H0; congr (_ + _ * _). rewrite /Omega /BCH_erreval; apply/polyP => i. rewrite !coef_sum supp_twisted //. apply eq_bigr => /= j jy. by rewrite !mxE mulr1. by rewrite -BCH_mod_is_GRS_mod. 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