proposition: Lemma cgen_dim (HC : not_trivial C) : let g := rVpoly (canonical_cgen HC) in \dim C = (n - (size g).-1)%nat.
proof: Proof. move=> g. Abort. Lemma divides_Xn_sub_1_is_linear (g : {poly F}) : g %| 'X^n - 1 -> submod_closed [set c : 'rV[F]_n | g %| rVpoly c] . Proof. case/dvdpP => /= i ig. split. by rewrite inE linear0 dvdp0. move=> k a b; rewrite !inE => ga gb. case/boolP : (k == 0) => [/eqP ->|k0]; first by rewrite scale0r add0r. by rewrite linearD linearZ /= dvdp_addr // dvdpZr. 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