proposition: Lemma dim_RS_code (a0 : a != 0) (auroot : not_uroot_on a n) : \dim (RS.code a n d) = (n - d)%N.
proof: Proof. apply dim_kernel; last by rewrite ltnW. rewrite -RS_GRS_PCM rank_GRS_PCM //. - by apply (@rVexp_inj _ _ _ a0 auroot). - by rewrite ltnW. - move=> i; by rewrite mxE expf_neq0. 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