fact: Definition erase (y : 'rV['F_2]_n) (E : {set 'I_n}) := \row_(n0 < n) if n0 \in E then Star else Bit (y ``_ n0).
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) f2 ssr_ext ssralg_ext max_subset num_occ hamming ldpc_erasure tanner linearcode