proposition: Lemma pgen_cgen (C_not_trivial : not_trivial C) (g : 'rV_n) : (rVpoly g \in 'pgen[[set cw in C]]) = (g \in 'cgen[C]).
proof: Proof. apply/idP/idP; [exact: pgen_is_cgen | exact: cgen_is_pgen]. 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