proposition: Lemma mxStarE i j : i \in 'F j -> mxStar i j = Star.
proof: Proof. rewrite /mxStar => ij; by rewrite mxE ij. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode