proposition: Lemma supp_neq0 n (F : fieldType) t (e : t.-'rV[F]_n) : supp e != set0 -> t != O.
proof: Proof. apply: contra => /eqP t0; case: e => /= e; by rewrite t0 leqn0 -cards_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft