proposition: Lemma syndromeE r y : syndrome r y = linearcode.syndrome (PCM r) y.
proof: Proof. apply/rowP => l; rewrite !mxE; apply/eq_bigr => /= i _. rewrite 2!mxE [in RHS]mulrC -mulrA; congr (_ * _). rewrite (bigD1 i) //= !mxE eqxx /= mulr1n mulrC. apply/eqP; rewrite addrC -subr_eq subrr; apply/eqP. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 // => j ji. by rewrite !mxE (negbTE ji) mulr0n mulr0. Qed.
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