fact: Definition distinct_non_zero (a : 'rV[F]_n) := injective [ffun i => a ``_i] /\ (forall i, a ``_ i != 0).
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft