proposition: Lemma PCM_GEN : Hamming.PCM m *m GEN ^T = 0.
proof: Proof. by rewrite /GEN tr_col_perm -mul_col_perm SysHamming.PCM_GEN'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel