proposition: Lemma PCM_alt_GRS : PCM_alt = GRS.PCM a a t.*2.
proof: Proof. apply/matrixP => i j. rewrite !mxE (bigD1 j) //= !mxE eqxx mulr1n exprS mulrC. 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 poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2