proposition: Lemma mem_poly_rV k (f : 'I_k -> {poly F}) : (forall i, poly_rV (f i) \in C) -> poly_rV (\big[+%R/0]_(i < k) (f i)) \in C.
proof: Proof. elim: k f => [f ? /= | ? IH f ?]. - by rewrite big_ord0 linear0 mem0v. - by rewrite big_ord_recl linearD /= (proj2 aclosed) // IH. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code