proposition: Lemma BCH_codebook (c : 'rV['F_2]_n) : (c \in BCHcode) = [forall j : 'I_t, (map_mx (@GF2_of_F2 m) c) ^`_(rVexp a n, inord j.*2.+1) == 0].
proof: Proof. apply/idP/idP. - case: BCHcode => code condition /= /condition. rewrite mem_kernel_syndrome0 -trmx0 => /eqP/trmx_inj/matrixP Hc. apply/forallP => /= i; apply/eqP; rewrite /fdcoor horner_poly. move: (Hc i ord0); rewrite !mxE => H1; rewrite -[RHS]H1. apply/eq_bigr => /= j _; rewrite insubT // => jn. rewrite mulrC 3![in RHS]mxE; congr (_ * (map_mx _ c) ord0 _); last by apply val_inj. rewrite inordK //; last first. move: (ltn_ord i). rewrite -(@ltn_pmul2r 2) // !muln2 -(ltn_add2r 1) !addn1. move/leq_trans; apply. move: tn. rewrite -divn2 leq_divRL // muln2. move/leq_ltn_trans; by apply. by rewrite exprAC. - move/forallP => H. case: BCHcode => code condition /=; apply (proj2 (condition _)). rewrite mem_kernel_syndrome0; apply/eqP/rowP => i; rewrite !mxE. rewrite -[RHS](eqP (H i)) /fdcoor horner_poly; apply/eq_bigr => /= j _. rewrite insubT // => jn. rewrite !mxE mulrC; congr (GF2_of_F2 (c ord0 _) * _); first by apply val_inj. rewrite inordK //; first by rewrite exprAC. move: (ltn_ord i). rewrite -(@ltn_pmul2r 2) // !muln2 -(ltn_add2r 1) !addn1. move/leq_trans; apply. move: tn. rewrite -divn2 leq_divRL // muln2 => /leq_ltn_trans; exact. 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