Mathlib.Algebra.Module.BigOperators

List.sum_smul theorem

{l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum

Full source

theorem List.sum_smul {l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
  map_list_sum ((smulAddHom R M).flip x) l

Distributivity of Scalar Multiplication over List Sums: $(\sum l) \bullet x = \sum_{r \in l} r \bullet x$

Informal description

For any list $l$ of elements in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiplication of the sum of $l$ by $x$ is equal to the sum of the scalar multiplications of each element in $l$ by $x$, i.e., \[ \left(\sum_{r \in l} r\right) \bullet x = \sum_{r \in l} (r \bullet x). \]

Multiset.sum_smul theorem

{l : Multiset R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum

Full source

theorem Multiset.sum_smul {l : Multiset R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
  ((smulAddHom R M).flip x).map_multiset_sum l

Distributivity of Scalar Multiplication over Multiset Sums: $(\sum l) \cdot x = \sum_{r \in l} r \cdot x$

Informal description

For any multiset $l$ of elements in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiplication of the sum of $l$ by $x$ is equal to the sum of the scalar multiplications of each element in $l$ by $x$, i.e., \[ \left(\sum_{r \in l} r\right) \cdot x = \sum_{r \in l} (r \cdot x). \]

Multiset.sum_smul_sum theorem

{s : Multiset R} {t : Multiset M} : s.sum • t.sum = ((s ×ˢ t).map fun p : R × M ↦ p.fst • p.snd).sum

Full source

theorem Multiset.sum_smul_sum {s : Multiset R} {t : Multiset M} :
    s.sum • t.sum = ((s ×ˢ t).map fun p : R × M ↦ p.fst • p.snd).sum := by
  induction' s using Multiset.induction with a s ih
  · simp
  · simp [add_smul, ih, ← Multiset.smul_sum]

Distributivity of Scalar Multiplication over Sums of Multisets: $\left(\sum s\right) \bullet \left(\sum t\right) = \sum_{(r, x) \in s \times t} r \bullet x$

Informal description

For any multisets $s$ of elements in a semiring $R$ and $t$ of elements in an $R$-module $M$, the scalar multiplication of the sum of $s$ by the sum of $t$ is equal to the sum of the scalar multiplications of all pairs $(r, x) \in s \times t$, i.e., \[ \left(\sum_{r \in s} r\right) \bullet \left(\sum_{x \in t} x\right) = \sum_{(r, x) \in s \times t} r \bullet x. \]

Finset.sum_smul theorem

{f : ι → R} {s : Finset ι} {x : M} : (∑ i ∈ s, f i) • x = ∑ i ∈ s, f i • x

Full source

theorem Finset.sum_smul {f : ι → R} {s : Finset ι} {x : M} :
    (∑ i ∈ s, f i) • x = ∑ i ∈ s, f i • x := map_sum ((smulAddHom R M).flip x) f s

Distributivity of Finite Sums over Scalar Multiplication in Modules

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any function $f : \iota \to R$, finite subset $s \subseteq \iota$, and element $x \in M$, we have $$\left(\sum_{i \in s} f(i)\right) \cdot x = \sum_{i \in s} f(i) \cdot x$$ where $\cdot$ denotes the scalar multiplication in $M$.

Finset.sum_smul_sum theorem

 (s : Finset α) (t : Finset β) {f : α → R} {g : β → M} : (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j

Full source

lemma Finset.sum_smul_sum (s : Finset α) (t : Finset β) {f : α → R} {g : β → M} :
    (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j := by
  simp_rw [sum_smul, ← smul_sum]

Distributivity of Scalar Multiplication over Double Finite Sums in Modules: $\left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{j \in t} g(j)\right) = \sum_{i \in s} \sum_{j \in t} f(i) \cdot g(j)$

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any functions $f : \alpha \to R$ and $g : \beta \to M$, we have \[ \left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{j \in t} g(j)\right) = \sum_{i \in s} \sum_{j \in t} f(i) \cdot g(j), \] where $\cdot$ denotes the scalar multiplication in $M$.

Fintype.sum_smul_sum theorem

[Fintype α] [Fintype β] (f : α → R) (g : β → M) : (∑ i, f i) • ∑ j, g j = ∑ i, ∑ j, f i • g j

Full source

lemma Fintype.sum_smul_sum [Fintype α] [Fintype β] (f : α → R) (g : β → M) :
    (∑ i, f i) • ∑ j, g j = ∑ i, ∑ j, f i • g j := Finset.sum_smul_sum _ _

Distributivity of Scalar Multiplication over Double Sums in Finite Types: $(\sum f) \cdot (\sum g) = \sum \sum f \cdot g$

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any finite types $\alpha$ and $\beta$, and any functions $f \colon \alpha \to R$ and $g \colon \beta \to M$, we have \[ \left(\sum_{i \in \alpha} f(i)\right) \cdot \left(\sum_{j \in \beta} g(j)\right) = \sum_{i \in \alpha} \sum_{j \in \beta} f(i) \cdot g(j), \] where $\cdot$ denotes the scalar multiplication in $M$.

Finset.cast_card theorem

[NonAssocSemiring R] (s : Finset α) : (#s : R) = ∑ _ ∈ s, 1

Full source

theorem Finset.cast_card [NonAssocSemiring R] (s : Finset α) : (#s : R) = ∑ _ ∈ s, 1 := by
  rw [Finset.sum_const, Nat.smul_one_eq_cast]

Cardinality as Sum of Ones in Non-Associative Semiring

Informal description

For any finite set $s$ and any non-associative semiring $R$, the canonical embedding of the cardinality of $s$ into $R$ equals the sum of the multiplicative identity over all elements in $s$, i.e., \[ |s| = \sum_{x \in s} 1, \] where $|s|$ denotes the cardinality of $s$ and $1$ is the multiplicative identity in $R$.

Fintype.sum_piFinset_apply theorem

 (f : κ → α) (s : Finset κ) (i : ι) : ∑ g ∈ piFinset fun _ : ι ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Full source

lemma sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) :
    ∑ g ∈ piFinset fun _ : ι ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b := by
  classical
  rw [Finset.sum_comp]
  simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
    Finset.sum_ite_mem, inter_self]

Sum over Functions with Fixed Component: $\sum_{g \in \prod s} f(g(i)) = |s|^{|\iota| - 1} \cdot \sum_{b \in s} f(b)$

Informal description

Let $\iota$ and $\kappa$ be finite types, $s$ be a finite subset of $\kappa$, and $f \colon \kappa \to \alpha$ be a function. For any fixed index $i \in \iota$, the sum of $f(g(i))$ over all functions $g \in \prod_{j \in \iota} s$ equals $|s|^{|\iota| - 1}$ times the sum of $f(b)$ over all $b \in s$. That is, \[ \sum_{g \in \prod_{j \in \iota} s} f(g(i)) = |s|^{|\iota| - 1} \cdot \sum_{b \in s} f(b). \]