Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Multiset.prod definition

: Multiset α → α

Full source

/-- Product of a multiset given a commutative monoid structure on `α`.
  `prod {a, b, c} = a * b * c` -/
@[to_additive
      "Sum of a multiset given a commutative additive monoid structure on `α`.
      `sum {a, b, c} = a + b + c`"]
def prod : Multiset α → α :=
  foldr (· * ·) 1

Product of elements in a multiset

Informal description

Given a commutative monoid structure on a type $\alpha$, the function `Multiset.prod` computes the product of all elements in a multiset $s$ of type $\alpha$. For example, $\text{prod} \{a, b, c\} = a \cdot b \cdot c$.

Multiset.prod_eq_foldr theorem

(s : Multiset α) : prod s = foldr (· * ·) 1 s

Full source

@[to_additive]
theorem prod_eq_foldr (s : Multiset α) :
    prod s = foldr (· * ·) 1 s :=
  rfl

Product of Multiset as Right Fold with Multiplication

Informal description

For any multiset $s$ over a type $\alpha$ with a commutative monoid structure, the product of all elements in $s$ is equal to the right fold of the multiplication operation over $s$ with initial value $1$. That is, $\prod s = \text{foldr} (\cdot) 1 s$.

Multiset.prod_eq_foldl theorem

(s : Multiset α) : prod s = foldl (· * ·) 1 s

Full source

@[to_additive]
theorem prod_eq_foldl (s : Multiset α) :
    prod s = foldl (· * ·) 1 s :=
  (foldr_swap _ _ _).trans (by simp [mul_comm])

Product of Multiset as Left Fold with Multiplication

Informal description

For any multiset $s$ over a commutative monoid $\alpha$, the product of all elements in $s$ is equal to the left fold of the multiplication operation over $s$ with initial value $1$. That is, $\prod s = \text{foldl} (\cdot) 1 s$.

Multiset.prod_coe theorem

(l : List α) : prod ↑l = l.prod

Full source

@[to_additive (attr := simp, norm_cast)]
theorem prod_coe (l : List α) : prod ↑l = l.prod := rfl

Product of Multiset from List Equals Product of List

Informal description

For any list $l$ of elements in a commutative monoid $\alpha$, the product of the elements in the multiset constructed from $l$ is equal to the product of the elements in $l$, i.e., $\text{prod}(\{l\}) = \text{prod}(l)$.

Multiset.prod_toList theorem

(s : Multiset α) : s.toList.prod = s.prod

Full source

@[to_additive (attr := simp)]
theorem prod_toList (s : Multiset α) : s.toList.prod = s.prod := by
  conv_rhs => rw [← coe_toList s]
  rw [prod_coe]

Equality of List and Multiset Products: $\text{prod}(\text{toList}(s)) = \text{prod}(s)$

Informal description

For any multiset $s$ over a commutative monoid $\alpha$, the product of the elements in the list representation of $s$ is equal to the product of the elements in $s$ itself. That is, $\text{prod}(\text{toList}(s)) = \text{prod}(s)$.

Multiset.prod_zero theorem

: @prod α _ 0 = 1

Full source

@[to_additive (attr := simp)]
theorem prod_zero : @prod α _ 0 = 1 :=
  rfl

Product of Empty Multiset is One

Informal description

For any commutative monoid $\alpha$, the product of the elements in the empty multiset $0$ is equal to the multiplicative identity $1$, i.e., $\prod 0 = 1$.

Multiset.prod_cons theorem

(a : α) (s) : prod (a ::ₘ s) = a * prod s

Full source

@[to_additive (attr := simp)]
theorem prod_cons (a : α) (s) : prod (a ::ₘ s) = a * prod s :=
  foldr_cons _ _ _ _

Product of multiset insertion: $\prod (a \text{ ::ₘ } s) = a \cdot \prod s$

Informal description

Let $\alpha$ be a commutative monoid. For any element $a \in \alpha$ and any multiset $s$ over $\alpha$, the product of the elements in the multiset obtained by inserting $a$ into $s$ equals $a$ multiplied by the product of the elements in $s$. That is, $$ \prod (a \text{ ::ₘ } s) = a \cdot \prod s. $$

Multiset.prod_singleton theorem

(a : α) : prod { a } = a

Full source

@[to_additive (attr := simp)]
theorem prod_singleton (a : α) : prod {a} = a := by
  simp only [mul_one, prod_cons, ← cons_zero, eq_self_iff_true, prod_zero]

Product of Singleton Multiset: $\prod \{a\} = a$

Informal description

For any element $a$ in a commutative monoid $\alpha$, the product of the elements in the singleton multiset $\{a\}$ is equal to $a$, i.e., $\prod \{a\} = a$.

Multiset.prod_pair theorem

(a b : α) : ({ a, b } : Multiset α).prod = a * b

Full source

@[to_additive]
theorem prod_pair (a b : α) : ({a, b} : Multiset α).prod = a * b := by
  rw [insert_eq_cons, prod_cons, prod_singleton]

Product of Two-Element Multiset: $\prod \{a, b\} = a \cdot b$

Informal description

For any two elements $a$ and $b$ in a commutative monoid $\alpha$, the product of the elements in the multiset $\{a, b\}$ is equal to $a \cdot b$, i.e., $\prod \{a, b\} = a \cdot b$.

Multiset.prod_replicate theorem

(n : ℕ) (a : α) : (replicate n a).prod = a ^ n

Full source

@[to_additive (attr := simp)]
theorem prod_replicate (n : ℕ) (a : α) : (replicate n a).prod = a ^ n := by
  simp [replicate, List.prod_replicate]

Product of Replicated Multiset Equals Power: $\prod (\text{replicate}\ n\ a) = a^n$

Informal description

For any natural number $n$ and any element $a$ in a commutative monoid $\alpha$, the product of the multiset containing $n$ copies of $a$ is equal to $a$ raised to the power of $n$, i.e., $\prod (\text{replicate}\ n\ a) = a^n$.

Multiset.pow_count theorem

[DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).prod

Full source

@[to_additive]
theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).prod := by
  rw [filter_eq, prod_replicate]

Power of Count Equals Product of Filtered Multiset: $a^{\text{count}(a, s)} = \prod \text{filter } (x = a) \ s$

Informal description

Let $\alpha$ be a type with decidable equality and a commutative monoid structure. For any element $a \in \alpha$ and any multiset $s$ over $\alpha$, the power $a$ raised to the multiplicity of $a$ in $s$ is equal to the product of the multiset obtained by filtering $s$ to keep only the elements equal to $a$. In symbols: $$ a^{\text{count}(a, s)} = \prod \left( \text{filter } (x \mapsto x = a) \ s \right) $$

Multiset.prod_hom_rel theorem

 (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 1 1)
  (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) : r (s.map f).prod (s.map g).prod

Full source

@[to_additive]
theorem prod_hom_rel (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
    (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
    r (s.map f).prod (s.map g).prod :=
  Quotient.inductionOn s fun l => by
    simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

Preservation of Relation Under Multiset Product Homomorphism

Informal description

Let $M$ and $N$ be commutative monoids, and let $r : M \to N \to \mathrm{Prop}$ be a relation between them. Given a multiset $s$ of elements of type $\iota$, and functions $f : \iota \to M$ and $g : \iota \to N$, if the relation $r$ holds for the identity elements ($r(1,1)$) and is preserved under multiplication (i.e., for any $a \in \iota$, $b \in M$, $c \in N$, if $r(b,c)$ holds then $r(f(a) \cdot b, g(a) \cdot c)$ also holds), then the relation $r$ holds between the product of the multiset obtained by mapping $f$ over $s$ and the product of the multiset obtained by mapping $g$ over $s$. In symbols: \[ r(1,1) \land (\forall a\ b\ c, r(b,c) \to r(f(a) \cdot b, g(a) \cdot c)) \implies r\left(\prod (s.\mathrm{map}\ f), \prod (s.\mathrm{map}\ g)\right) \]

Multiset.prod_map_one theorem

: prod (m.map fun _ => (1 : α)) = 1

Full source

@[to_additive]
theorem prod_map_one : prod (m.map fun _ => (1 : α)) = 1 := by
  rw [map_const', prod_replicate, one_pow]

Product of Multiset Mapped to Identity Equals Identity: $\prod (m.\text{map} (\lambda \_, 1)) = 1$

Informal description

For any multiset $m$ over a commutative monoid $\alpha$, the product of the multiset obtained by mapping every element of $m$ to the multiplicative identity $1$ is equal to $1$, i.e., $\prod (m.\text{map} (\lambda \_, 1)) = 1$.

Multiset.prod_induction theorem

 (p : α → Prop) (s : Multiset α) (p_mul : ∀ a b, p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p s.prod

Full source

@[to_additive]
theorem prod_induction (p : α → Prop) (s : Multiset α) (p_mul : ∀ a b, p a → p b → p (a * b))
    (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p s.prod := by
  rw [prod_eq_foldr]
  exact foldr_induction (· * ·) 1 p s p_mul p_one p_s

Induction Principle for Multiset Products

Informal description

Let $\alpha$ be a commutative monoid, $s$ a multiset over $\alpha$, and $p$ a predicate on $\alpha$. If: 1. $p$ is multiplicative (i.e., $p(a) \land p(b) \implies p(a \cdot b)$ for all $a, b \in \alpha$), 2. $p(1)$ holds, and 3. $p(a)$ holds for all $a \in s$, then $p(\prod s)$ holds, where $\prod s$ denotes the product of all elements in $s$.

Multiset.prod_induction_nonempty theorem

(p : α → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p s.prod

Full source

@[to_additive]
theorem prod_induction_nonempty (p : α → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅)
    (p_s : ∀ a ∈ s, p a) : p s.prod := by
  induction s using Multiset.induction_on with
  | empty => simp at hs
  | cons a s hsa =>
    rw [prod_cons]
    by_cases hs_empty : s = ∅
    · simp [hs_empty, p_s a]
    have hps : ∀ x, x ∈ s → p x := fun x hxs => p_s x (mem_cons_of_mem hxs)
    exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

Induction Principle for Products over Nonempty Multisets

Informal description

Let $\alpha$ be a commutative monoid, $s$ a nonempty multiset over $\alpha$, and $p$ a predicate on $\alpha$. If $p$ holds for all elements of $s$ and is preserved under multiplication (i.e., $p(a) \land p(b) \implies p(a \cdot b)$ for all $a, b \in \alpha$), then $p$ holds for the product of all elements in $s$.

Main declarations