fact: Definition vproj n (F : ringType) (x : 'rV[F]_n) (s : {set 'I_n}) := \row_(i < n) if i \in s then x ord0 i else 0.
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