proposition: Lemma kernel_checksubsum1 (x : 'rV['F_2]_n) : x \in kernel H -> (1 = (\prod_m0 \delta ('V m0) x)%:R)%R.
proof: Proof. move=> x_in_C. rewrite {1}(_ : (1 = (\prod_(m0 < m) 1)%:R)%R); [congr INR | by rewrite big_const iter_muln_1 exp1n]. apply eq_bigr => m0 _. rewrite /C mem_kernel_syndrome0 /syndrome in x_in_C. move/eqP in x_in_C. have {}x_in_C : forall m0, \sum_i (H m0 i) * (x ``_ i) = 0. move=> m1. move/rowP : x_in_C => /(_ m1). rewrite !mxE. move=> t_in_C; rewrite -[in X in _ = X]t_in_C. apply eq_bigr => // i _; congr (_ * _). by rewrite /row_of_tuple !mxE. have {}x_in_C : forall m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) = 0. move=> m1. rewrite -[in X in _ = X](x_in_C m1); symmetry. rewrite (bigID [pred i | i \in 'V m1]) /=. set tmp := {2}(\sum_(i in 'V m1) _). rewrite -[in X in _ = X](addr0 tmp); congr (_ + _). rewrite [in X in _ = X](_ : 0 = \sum_(i | i \notin 'V m1) 0); last first. by rewrite big_const /= iter_addr0. apply eq_big => // n0. rewrite VnextE tanner_relE -F2_eq0 => /eqP ->; by rewrite mul0r. have {}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0. move=> m1. rewrite -[in X in _ = X](x_in_C m1). apply eq_bigr => // i. rewrite VnextE tanner_relE => /eqP ->; by rewrite mul1r. have {}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0. move=> m1. by rewrite -{2}(x_in_C m1). by rewrite /checksubsum (x_in_C m0) eqxx. 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