proposition: Lemma S1_Convn n (g : 'I_n -> T) d : S1 (<|>_d g) = \ssum_(i < n) scalept (d i) (S1 (g i)).
proof: Proof. by rewrite (S1_Convn_proj [the {affine _ ->_} of idfun]). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist