proposition: Lemma dual_codeP2 y : (forall x, x \in kernel H -> y *m x^T = 0) -> y \in dual_code.
proof: Proof. move=> /= H0. suff [l Hl] : exists l : 'rV_m, y = \sum_(j < m) (l ord0 j) *: (row j H). apply/memv_imgP; exists l. by rewrite memvf. by rewrite lfunE /= Hl mulmx_sum_row. Abort. End dual_code. Section not_trivial_code_properties. Variables (F : finFieldType) (n : nat) (C : Lcode0.t F n). Hypothesis C_not_trivial : not_trivial C. Lemma not_trivial_dim : 0 < \dim C. Proof. rewrite lt0n dimv_eq0; by apply not_trivialP. 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