proposition: Lemma scaler_closed : GRing.scaler_closed codebook.
proof: Proof. move=> k x; rewrite !inE => /forallP xC. apply/forallP => /= i; apply/implyP => i0. rewrite tdcoorZ; move: (xC i); rewrite i0 implyTb => /eqP ->; by rewrite mulr0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code