proposition: Lemma map_mx_rcs (R0 R1 : idomainType) n (x : 'rV[R0]_n.+1) (f : R0 -> R1) : map_mx f (rcs x) = rcs (map_mx f x).
proof: Proof. by rewrite /rcs map_col_perm. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft