fact: Definition BCH_mod (y : 'rV[F]_n) : {poly F} := \sum_(i in supp y) y ``_ i *: (\prod_(j in supp y :\ i) (1 - a ^+ j *: 'X) * - (a ^+ (t.*2.+1 * i))%:P).
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