proposition: Lemma dim_dual_code : (\dim (kernel H) + \dim dual_code = n)%N.
proof: Proof. move: (limg_ker_dim (linfun (lin_syndrome H)) fullv). rewrite -/(kernel H). rewrite (_ : (fullv :&: _)%VS = kernel H); last by apply/capv_idPr/subvf. rewrite (_ : \dim fullv = n); last by rewrite dimvf /Vector.dim /= mul1n. rewrite (_ : \dim (limg _) = \dim dual_code) // /dual_code. rewrite /dimv. Abort. Lemma dual_codeP1 y : y \in dual_code -> (forall x, x \in kernel H -> y *m x^T = 0). Proof. case/memv_imgP => y' _. rewrite !lfunE => ->{y} x. rewrite memv_ker => /eqP. rewrite lfunE /= /syndrome => /(congr1 trmx). rewrite trmx0 trmxK -mulmxA => ->; by rewrite mulmx0. 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