fact: Definition BCH_err y : {poly 'F_2} := let r0 : {poly F} := 'X^t.*2 in let r1 := \BCHsynp_(rVexp a n, y, t) in let vstop := v r0 r1 (stop t r0 r1) in let s := vstop.[0]^-1 *: vstop in \poly_(i < n) (if s.[a^- i] == 0 then 1 else 0).
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