Mathlib.Algebra.BigOperators.Ring.Multiset

Multiset.prod_map_neg theorem

(s : Multiset α) : (s.map Neg.neg).prod = (-1) ^ card s * s.prod

Full source

@[simp] lemma prod_map_neg (s : Multiset α) : (s.map Neg.neg).prod = (-1) ^ card s * s.prod :=
  Quotient.inductionOn s (by simp)

Product of Negated Multiset Equals $(-1)^{|s|}$ Times Original Product

Informal description

For any multiset $s$ over a commutative monoid $\alpha$, the product of the multiset obtained by negating each element of $s$ is equal to $(-1)^{|s|}$ multiplied by the product of the original multiset $s$, i.e., $$\prod_{x \in s} (-x) = (-1)^{|s|} \cdot \prod_{x \in s} x.$$

Multiset.prod_eq_zero theorem

(h : (0 : α) ∈ s) : s.prod = 0

Full source

lemma prod_eq_zero (h : (0 : α) ∈ s) : s.prod = 0 := by
  rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩; simp [hs', Multiset.prod_cons]

Product of Multiset Containing Zero is Zero

Informal description

For any multiset $s$ over a type $\alpha$ with a zero element and a multiplication operation, if $0 \in s$, then the product of all elements in $s$ is equal to $0$.

Multiset.prod_eq_zero_iff theorem

: s.prod = 0 ↔ (0 : α) ∈ s

Full source

@[simp] lemma prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
  Quotient.inductionOn s fun l ↦ by rw [quot_mk_to_coe, prod_coe]; exact List.prod_eq_zero_iff

Product of Multiset Equals Zero if and only if it Contains Zero

Informal description

For any multiset $s$ of elements in a monoid with zero $\alpha$, the product of all elements in $s$ equals zero if and only if $s$ contains the zero element, i.e., $\prod s = 0 \leftrightarrow 0 \in s$.

Multiset.prod_ne_zero theorem

(h : (0 : α) ∉ s) : s.prod ≠ 0

Full source

lemma prod_ne_zero (h : (0 : α) ∉ s) : s.prod ≠ 0 := mt prod_eq_zero_iff.1 h

Nonzero Product of Zero-Free Multiset

Informal description

For any multiset $s$ over a type $\alpha$ with a zero element and a multiplication operation, if $0$ is not an element of $s$, then the product of all elements in $s$ is not equal to $0$.

Multiset.sum_map_mul_left theorem

: sum (s.map fun i ↦ a * f i) = a * sum (s.map f)

Full source

lemma sum_map_mul_left : sum (s.map fun i ↦ a * f i) = a * sum (s.map f) :=
  Multiset.induction_on s (by simp) fun i s ih => by simp [ih, mul_add]

Left Multiplicative Factor Commutes with Multiset Summation

Informal description

For any multiset $s$ over a type $\alpha$, any function $f : \alpha \to \beta$ (where $\beta$ is a type with multiplication and addition), and any element $a \in \beta$, the sum of the multiset obtained by mapping each element $i \in s$ to $a \cdot f(i)$ is equal to $a$ multiplied by the sum of the multiset obtained by mapping $f$ over $s$. In symbols: \[ \sum_{i \in s} (a \cdot f(i)) = a \cdot \left( \sum_{i \in s} f(i) \right). \]

Multiset.sum_map_mul_right theorem

: sum (s.map fun i ↦ f i * a) = sum (s.map f) * a

Full source

lemma sum_map_mul_right : sum (s.map fun i ↦ f i * a) = sum (s.map f) * a :=
  Multiset.induction_on s (by simp) fun a s ih => by simp [ih, add_mul]

Right Multiplicative Summation over a Multiset

Informal description

For any multiset $s$ over a type $\alpha$, any function $f : \alpha \to \beta$ where $\beta$ is a multiplicative semigroup, and any element $a \in \beta$, the sum of the multiset obtained by mapping each element $i \in s$ to $f(i) * a$ is equal to the sum of the multiset obtained by mapping $f$ over $s$ multiplied by $a$. That is, \[ \sum_{i \in s} (f(i) * a) = \left(\sum_{i \in s} f(i)\right) * a. \]

Multiset.dvd_sum theorem

: (∀ x ∈ s, a ∣ x) → a ∣ s.sum

Full source

lemma dvd_sum : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
  Multiset.induction_on s (fun _ ↦ dvd_zero _) fun x s ih h ↦ by
    rw [sum_cons]
    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

Divisibility of Sum by Common Divisor in Multisets

Informal description

For any multiset $s$ over a type $\alpha$ with a divisibility relation $\mid$ and a sum operation, if an element $a$ divides every element $x$ in $s$, then $a$ divides the sum of all elements in $s$.

Multiset.prod_map_sum theorem

{s : Multiset (Multiset α)} : prod (s.map sum) = sum ((Sections s).map prod)

Full source

lemma prod_map_sum {s : Multiset (Multiset α)} :
    prod (s.map sum) = sum ((Sections s).map prod) :=
  Multiset.induction_on s (by simp) fun a s ih ↦ by
    simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]

Product of Sums Equals Sum of Products for Multiset Sections

Informal description

For any multiset $s$ of multisets over a type $\alpha$ with a commutative multiplication and addition, the product of the sums of each multiset in $s$ is equal to the sum of the products of all sections of $s$. That is, \[ \prod_{m \in s} \left( \sum_{x \in m} x \right) = \sum_{t \in \text{Sections}(s)} \left( \prod_{y \in t} y \right). \]

Multiset.prod_map_add theorem

 {s : Multiset ι} {f g : ι → α} :
  prod (s.map fun i ↦ f i + g i) = sum ((antidiagonal s).map fun p ↦ (p.1.map f).prod * (p.2.map g).prod)

Full source

lemma prod_map_add {s : Multiset ι} {f g : ι → α} :
    prod (s.map fun i ↦ f i + g i) =
      sum ((antidiagonal s).map fun p ↦ (p.1.map f).prod * (p.2.map g).prod) := by
  refine s.induction_on ?_ fun a s ih ↦ ?_
  · simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
  · simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
      mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd,
      id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]
    exact add_comm _ _

Product-to-Sum Expansion for Multiset Maps: $\prod (f + g) = \sum_{t_1 + t_2 = s} \prod f(t_1) \cdot \prod g(t_2)$

Informal description

Let $s$ be a multiset over a type $\iota$, and let $f, g : \iota \to \alpha$ be functions where $\alpha$ is a commutative semiring. Then the product of the multiset obtained by mapping each element $i \in s$ to $f(i) + g(i)$ is equal to the sum over all pairs $(t_1, t_2)$ in the antidiagonal of $s$ of the product of the image of $t_1$ under $f$ and the image of $t_2$ under $g$. In symbols: \[ \prod_{i \in s} (f(i) + g(i)) = \sum_{(t_1, t_2) \in \mathrm{antidiagonal}(s)} \left( \prod_{a \in t_1} f(a) \right) \cdot \left( \prod_{b \in t_2} g(b) \right). \]

Commute.multiset_sum_right theorem

(a : α) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum

Full source

theorem multiset_sum_right (a : α) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum := by
  induction s using Quotient.inductionOn
  rw [quot_mk_to_coe, sum_coe]
  exact Commute.list_sum_right _ _ h

Commutation of an Element with the Sum of a Commuting Multiset

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $s$ be a multiset of elements of $\alpha$. If an element $a \in \alpha$ commutes with every element $b \in s$ (i.e., $a * b = b * a$ for all $b \in s$), then $a$ commutes with the sum of the multiset $s$.

Commute.multiset_sum_left theorem

(b : α) (h : ∀ a ∈ s, Commute a b) : Commute s.sum b

Full source

theorem multiset_sum_left (b : α) (h : ∀ a ∈ s, Commute a b) : Commute s.sum b :=
  ((Commute.multiset_sum_right _ _) fun _ ha => (h _ ha).symm).symm

Commutation of Multiset Sum with a Commuting Element

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $s$ be a multiset of elements of $\alpha$. If an element $b \in \alpha$ commutes with every element $a \in s$ (i.e., $a * b = b * a$ for all $a \in s$), then the sum of the multiset $s$ commutes with $b$.