Finite sums over modules over a ring #
theorem
Finset.sum_smul
{ι : Type u_1}
{R : Type u_5}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{f : ι → R}
{s : Finset ι}
{x : M}
:
theorem
Fintype.sum_piFinset_apply
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[DecidableEq ι]
[Fintype ι]
[AddCommMonoid α]
(f : κ → α)
(s : Finset κ)
(i : ι)
: