proposition: Lemma syndromepD x y : syndromep u (x + y) t = syndromep u x t + syndromep u y t.
proof: Proof. rewrite /syndromep !poly_def -big_split /=; apply/eq_bigr => i _. by rewrite fdcoorD scalerDl. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft