proposition: Lemma Prod_mxStar_col_Star n0 (s : {set 'I_m}) : Prod [seq (col n0 mxStar) m0 ord0 | m0 in s] = Star.
proof: Proof. rewrite Prod_starblank_is_Star //=; apply/allP => y' /mapP [x Hx ->]. rewrite 2!mxE; by case: ifPn. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode