proposition: Lemma checksubsum_in_kernel (x : 'rV['F_2]_n) : (\prod_(i < m) (\delta ('V i) x)%:R = (x \in kernel H)%:R)%R.
proof: Proof. rewrite kernel_checksubsum. transitivity ((\prod_m1 (\delta ('V m1) x))%:R)%R. by rewrite -big_morph_natRM. congr (_%:R). erewrite (@big_morph _ _ nat_of_bool true) => //. move=> ? ? /=; by rewrite mulnb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector) Reals ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode pproba