fact: Definition summary_powerset (X : {set 'I_n}) (d : 'rV['F_2]_n) (e : 'rV_n -> R) := let bvect s := \row_(i < n) if i \in X then F2_of_bool (i \in s) else d ``_ i in \sum_(s in powerset X) e (bvect s).
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2