Finite sums over modules over a ring #
theorem
Multiset.sum_smul
{R : Type u_5}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{l : Multiset R}
{x : M}
:
Multiset.sum l • x = Multiset.sum (Multiset.map (fun (r : R) => r • x) l)
theorem
Multiset.sum_smul_sum
{R : Type u_5}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Multiset R}
{t : Multiset M}
:
Multiset.sum s • Multiset.sum t = Multiset.sum (Multiset.map (fun (p : R × M) => p.1 • p.2) (s ×ˢ t))
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}
:
(Finset.sum s fun (i : ι) => f i) • x = Finset.sum s fun (i : ι) => f i • x
theorem
Finset.sum_smul_sum
{α : Type u_3}
{β : Type u_4}
{R : Type u_5}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{f : α → R}
{g : β → M}
{s : Finset α}
{t : Finset β}
:
((Finset.sum s fun (i : α) => f i) • Finset.sum t fun (i : β) => g i) = Finset.sum (s ×ˢ t) fun (p : α × β) => f p.1 • g p.2
theorem
Finset.cast_card
{α : Type u_3}
{R : Type u_5}
[CommSemiring R]
(s : Finset α)
:
↑s.card = Finset.sum s fun (a : α) => 1
theorem
Fintype.sum_piFinset_apply
{ι : Type u_1}
{κ : Type u_2}
{α : Type u_3}
[DecidableEq ι]
[Fintype ι]
[AddCommMonoid α]
(f : κ → α)
(s : Finset κ)
(i : ι)
:
(Finset.sum (Fintype.piFinset fun (x : ι) => s) fun (g : ι → κ) => f (g i)) = s.card ^ (Fintype.card ι - 1) • Finset.sum s fun (b : κ) => f b