proposition: Lemma cgen_is_pgen g : g \in 'cgen[C] -> rVpoly g \in 'pgen[[set cw in C]].
proof: Proof. move=> Hg; apply/forallP => p; apply/eqP; apply/idP/idP => [p_in_C | g_generated]. - have H : poly_rV (`[ rVpoly p ]_n) = p. by rewrite modp_small // ?rVpolyK // size_Xn_sub_1 // ltnS size_poly. rewrite -{}H in p_in_C. apply divide_codeword => //; by rewrite inE in p_in_C. - case/dvdpP: g_generated => /= i p_i_g. rewrite -(rVpolyK p). have <- : `[ rVpoly p ]_n = rVpoly p. rewrite modp_small // size_Xn_sub_1 // ltnS; by apply size_poly. rewrite p_i_g inE shift_linearity_codeword //. by apply (size_is_cgen Hg). by rewrite rVpolyK //; case/and3P : Hg. 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