proposition: Lemma RS_GRS_PCM : GRS.PCM b b d = RS.PCM a n d.
proof: Proof. apply/matrixP => i j. rewrite !mxE (bigD1 j) //= !mxE eqxx mulr1n -exprSr -exprM mulnC exprM. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addr0 ?addr0 // => k kj. by rewrite !mxE (negbTE kj) mulr0n 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