fact: Definition beta n0 m0 (d : 'rV_n) := W (d ``_ n0) (y ``_ n0) * \prod_(m1 in 'F n0 :\ m0) alpha m1 n0 d.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext fdist channel pproba f2 linearcode subgraph_partition tanner tanner_partition hamming binary_symmetric_channel decoding channel_code summary checksum summary_tanner