proposition: Lemma syndromep_t0 (F : fieldType) n (a : 'rV[F]_n.+1) e : syndromep a e 0 = 0.
proof: Proof. by rewrite /syndromep poly_def big_ord0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft