fact: Definition lin_syndrome : {linear 'rV[F]_n -> 'rV[F]_m} := GRing.Linear.Pack _ (GRing.Linear.Class additive_syndrome syndromeZ).
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