fact: Definition syndrome_coord (i : nat) (y : 'rV_n) := \sum_(j < n) y ``_ j * b ``_ j * (a ``_ j) ^+ i.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext vandermonde linearcode dft poly_decoding