proposition: Lemma tdcoorZ k x i : (k *: x) ^`_ i = k * x ^`_ i.
proof: Proof. by rewrite /fdcoor linearZ /= hornerZ. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming