proposition: Lemma shift_linearity_codeword (c : {poly F}) (cn : size c <= n) : poly_rV c \in C -> forall p, poly_rV (`[ p * c ]_ n) \in C.
proof: Proof. move=> /= cC p; rewrite -(coefK p). have -> : \poly_(i < size p) p`_i * c = \sum_(i < size p) (p`_i *: ('X^i * c)). rewrite mulrC poly_def big_distrr /=. apply eq_bigr => k _; by rewrite mulrC scalerAl. have -> : `[ \sum_(i < size p) (p`_i *: ('X^i * c)) ]_n = \sum_(i < size p) `[ p`_i *: ('X^i * c) ]_n. by rewrite (big_morph (id1 := 0) _ (@morph_modp _ _)) // mod0p. have -> : \sum_(i < size p) `[ p`_i *: ('X^i * c) ]_n = \sum_(i < size p) (p`_i *: `[ 'X^i * c ]_ n ). apply eq_bigr => k _; by rewrite modpZl. apply Lcode0.mem_poly_rV => j. rewrite linearZ /= Lcode0.sclosed //; by apply shift_codeword. 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