proposition: Lemma PCM_lin1_mx : RS.PCM a n d = (lin1_mx (linfun (lin_syndrome (RS.PCM a n d))))^T.
proof: Proof. apply/matrixP => i j. rewrite !(mxE,lfunE) (bigD1 j) //= !mxE !eqxx mulr1 (eq_bigr (fun=> 0)). - by rewrite big_const iter_addr0 addr0. - move=> k kj; by rewrite !mxE eqxx (negbTE kj) mulr0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code