Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Multiset.prod_erase theorem

[DecidableEq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod

Full source

@[to_additive (attr := simp)]
theorem prod_erase [DecidableEq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod := by
  rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]

Product of Multiset Equals Element Times Product After Erasure

Informal description

Let $\alpha$ be a type with decidable equality and $M$ a commutative monoid. For any multiset $s$ over $\alpha$ and any element $a \in s$, the product of $s$ is equal to $a$ multiplied by the product of the multiset obtained by removing one occurrence of $a$ from $s$, i.e., \[ a \cdot \left(\prod_{x \in \text{erase}(s, a)} x\right) = \prod_{x \in s} x. \]

Multiset.prod_map_erase theorem

[DecidableEq ι] {a : ι} (h : a ∈ m) : f a * ((m.erase a).map f).prod = (m.map f).prod

Full source

@[to_additive (attr := simp)]
theorem prod_map_erase [DecidableEq ι] {a : ι} (h : a ∈ m) :
    f a * ((m.erase a).map f).prod = (m.map f).prod := by
  rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe,
    List.prod_map_erase f (mem_toList.2 h)]

Product Preservation under Element Removal and Mapping in Multisets

Informal description

Let $\iota$ be a type with decidable equality, $M$ a commutative monoid, $f : \iota \to M$ a function, $m$ a multiset over $\iota$, and $a \in \iota$ an element such that $a \in m$. Then: \[ f(a) \cdot \left(\prod_{x \in \text{erase}(m, a)} f(x)\right) = \prod_{x \in m} f(x) \] where $\text{erase}(m, a)$ denotes the multiset obtained by removing one occurrence of $a$ from $m$.

Multiset.prod_add theorem

(s t : Multiset α) : prod (s + t) = prod s * prod t

Full source

@[to_additive (attr := simp)]
theorem prod_add (s t : Multiset α) : prod (s + t) = prod s * prod t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => by simp

Product of Sum of Multisets Equals Product of Parts

Informal description

For any two multisets $s$ and $t$ over a commutative monoid $\alpha$, the product of their sum $s + t$ is equal to the product of $s$ multiplied by the product of $t$, i.e., $\prod (s + t) = \prod s \cdot \prod t$.

Multiset.prod_nsmul theorem

(m : Multiset α) : ∀ n : ℕ, (n • m).prod = m.prod ^ n

Full source

@[to_additive]
theorem prod_nsmul (m : Multiset α) : ∀ n : ℕ, (n • m).prod = m.prod ^ n
  | 0 => by
    rw [zero_nsmul, pow_zero]
    rfl
  | n + 1 => by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

Product of Scaled Multiset Equals Power of Product: $\prod (n \cdot m) = (\prod m)^n$

Informal description

For any multiset $m$ over a commutative monoid $\alpha$ and any natural number $n$, the product of the multiset obtained by scaling $m$ by $n$ (i.e., adding $m$ to itself $n$ times) is equal to the $n$-th power of the product of $m$, i.e., \[ \prod (n \cdot m) = \left(\prod m\right)^n. \]

Multiset.prod_filter_mul_prod_filter_not theorem

(p) [DecidablePred p] : (s.filter p).prod * (s.filter (fun a ↦ ¬p a)).prod = s.prod

Full source

@[to_additive]
theorem prod_filter_mul_prod_filter_not (p) [DecidablePred p] :
    (s.filter p).prod * (s.filter (fun a ↦ ¬ p a)).prod = s.prod := by
  rw [← prod_add, filter_add_not]

Product Decomposition of a Multiset via Filtering: $\prod (s) = \prod (s \text{ filtered by } p) \cdot \prod (s \text{ filtered by } \neg p)$

Informal description

For any multiset $s$ over a commutative monoid $\alpha$ and any decidable predicate $p$ on $\alpha$, the product of the elements in $s$ that satisfy $p$ multiplied by the product of the elements in $s$ that do not satisfy $p$ equals the product of all elements in $s$. That is, \[ \left(\prod_{a \in \text{filter } p\ s} a\right) \cdot \left(\prod_{a \in \text{filter } (\neg p)\ s} a\right) = \prod_{a \in s} a. \]

Multiset.prod_map_eq_pow_single theorem

[DecidableEq ι] (i : ι) (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) : (m.map f).prod = f i ^ m.count i

Full source

@[to_additive]
theorem prod_map_eq_pow_single [DecidableEq ι] (i : ι)
    (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) : (m.map f).prod = f i ^ m.count i := by
  induction m using Quotient.inductionOn
  simp [List.prod_map_eq_pow_single i f hf]

Product of Mapped Multiset Equals Power of Single Element: $\prod (m \text{ mapped by } f) = f(i)^{\text{count}(i, m)}$

Informal description

Let $\iota$ be a type with decidable equality, $M$ a commutative monoid, $m$ a multiset over $\iota$, $i \in \iota$, and $f \colon \iota \to M$ a function such that for all $i' \in \iota$, if $i' \neq i$ and $i' \in m$, then $f(i') = 1$. Then the product of the multiset obtained by applying $f$ to each element of $m$ is equal to $f(i)$ raised to the power of the multiplicity of $i$ in $m$, i.e., \[ \prod_{x \in m} f(x) = f(i)^{\text{count}(i, m)}. \]

Multiset.prod_eq_pow_single theorem

[DecidableEq α] (a : α) (h : ∀ a' ≠ a, a' ∈ s → a' = 1) : s.prod = a ^ s.count a

Full source

@[to_additive]
theorem prod_eq_pow_single [DecidableEq α] (a : α) (h : ∀ a' ≠ a, a' ∈ s → a' = 1) :
    s.prod = a ^ s.count a := by
  induction s using Quotient.inductionOn; simp [List.prod_eq_pow_single a h]

Product of Multiset Equals Power of Single Non-Identity Element: $\prod s = a^{\text{count}(a, s)}$

Informal description

Let $\alpha$ be a commutative monoid with decidable equality, $s$ a multiset over $\alpha$, and $a \in \alpha$. If every element $a' \in s$ with $a' \neq a$ equals the multiplicative identity $1$, then the product of all elements in $s$ is equal to $a$ raised to the power of its multiplicity in $s$, i.e., \[ \prod_{x \in s} x = a^{\text{count}(a, s)}. \]

Multiset.prod_eq_one theorem

(h : ∀ x ∈ s, x = (1 : α)) : s.prod = 1

Full source

@[to_additive]
lemma prod_eq_one (h : ∀ x ∈ s, x = (1 : α)) : s.prod = 1 := by
  induction s using Quotient.inductionOn; simp [List.prod_eq_one h]

Product of Identity Elements in Multiset is Identity

Informal description

Let $s$ be a multiset over a commutative monoid $\alpha$. If every element $x$ in $s$ equals the multiplicative identity $1$, then the product of all elements in $s$ is also $1$.

Multiset.prod_hom_ne_zero theorem

 {s : Multiset α} (hs : s ≠ 0) {F : Type*} [FunLike F α β] [MulHomClass F α β] (f : F) : (s.map f).prod = f s.prod

Full source

@[to_additive]
theorem prod_hom_ne_zero {s : Multiset α} (hs : s ≠ 0) {F : Type*} [FunLike F α β]
    [MulHomClass F α β] (f : F) :
    (s.map f).prod = f s.prod := by
  induction s using Quot.inductionOn; aesop (add simp List.prod_hom_nonempty)

Homomorphism Property for Nonempty Multiset Products: $\prod f(x) = f(\prod x)$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplicative structures, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve multiplication. For any nonempty multiset $s$ over $\alpha$ and any homomorphism $f \in F$, the product of the image of $s$ under $f$ is equal to $f$ applied to the product of $s$, i.e., \[ \prod_{x \in s} f(x) = f\left(\prod_{x \in s} x\right). \]

Multiset.prod_hom theorem

(s : Multiset α) {F : Type*} [FunLike F α β] [MonoidHomClass F α β] (f : F) : (s.map f).prod = f s.prod

Full source

@[to_additive]
theorem prod_hom (s : Multiset α) {F : Type*} [FunLike F α β]
    [MonoidHomClass F α β] (f : F) :
    (s.map f).prod = f s.prod :=
  Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe]

Homomorphism Property for Multiset Products: $\prod f(x) = f(\prod x)$

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any multiset $s$ over $\alpha$, the product of the multiset obtained by applying $f$ to each element of $s$ is equal to $f$ applied to the product of $s$. That is, \[ \prod_{x \in s} f(x) = f\left(\prod_{x \in s} x\right). \]

Multiset.prod_hom' theorem

 (s : Multiset ι) {F : Type*} [FunLike F α β] [MonoidHomClass F α β] (f : F) (g : ι → α) :
  (s.map fun i => f <| g i).prod = f (s.map g).prod

Full source

@[to_additive]
theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F α β]
    [MonoidHomClass F α β] (f : F)
    (g : ι → α) : (s.map fun i => f <| g i).prod = f (s.map g).prod := by
  convert (s.map g).prod_hom f
  exact (map_map _ _ _).symm

Homomorphism Property for Multiset Products with Indexed Function: $\prod f(g(i)) = f(\prod g(i))$

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any multiset $s$ over an index type $\iota$ and any function $g \colon \iota \to \alpha$, the product of the multiset obtained by applying $f \circ g$ to each element of $s$ is equal to $f$ applied to the product of the multiset obtained by mapping $g$ over $s$. That is, \[ \prod_{i \in s} f(g(i)) = f\left(\prod_{i \in s} g(i)\right). \]

Multiset.prod_hom₂_ne_zero theorem

 [CommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d)
  (f₁ : ι → α) (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod

Full source

@[to_additive]
theorem prod_hom₂_ne_zero [CommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → α) (f₂ : ι → β) :
    (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod := by
  induction s using Quotient.inductionOn; aesop (add simp List.prod_hom₂_nonempty)

Product Homomorphism Property for Nonempty Multisets: $\prod_{i \in s} f(f_1(i), f_2(i)) = f\left(\prod_{i \in s} f_1(i), \prod_{i \in s} f_2(i)\right)$

Informal description

Let $\gamma$ be a commutative monoid, and let $s$ be a nonempty multiset over an index type $\iota$. Given a function $f : \alpha \to \beta \to \gamma$ satisfying the property that for all $a, b \in \alpha$ and $c, d \in \beta$, we have $f(a \cdot b, c \cdot d) = f(a, c) \cdot f(b, d)$, and functions $f_1 : \iota \to \alpha$ and $f_2 : \iota \to \beta$, the product of the multiset obtained by mapping each element $i \in s$ to $f(f_1(i), f_2(i))$ is equal to $f$ applied to the product of the multiset obtained by mapping $f_1$ over $s$ and the product of the multiset obtained by mapping $f_2$ over $s$. That is, \[ \prod_{i \in s} f(f_1(i), f_2(i)) = f\left(\prod_{i \in s} f_1(i), \prod_{i \in s} f_2(i)\right). \]

Multiset.prod_hom₂ theorem

 [CommMonoid γ] (s : Multiset ι) (f : α → β → γ) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1)
  (f₁ : ι → α) (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod

Full source

@[to_additive]
theorem prod_hom₂ [CommMonoid γ] (s : Multiset ι) (f : α → β → γ)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α)
    (f₂ : ι → β) : (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
  Quotient.inductionOn s fun l => by
    simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, map_coe, prod_coe]

Bilinear Product Formula for Multisets in Commutative Monoids

Informal description

Let $M$, $N$, $P$ be commutative monoids and let $f : M \to N \to P$ be a function satisfying: 1. For all $a, b \in M$ and $c, d \in N$, we have $f(a \cdot b, c \cdot d) = f(a, c) \cdot f(b, d)$. 2. $f(1_M, 1_N) = 1_P$. Then for any multiset $s$ over a type $\iota$ and functions $f_1 : \iota \to M$, $f_2 : \iota \to N$, the product of the multiset obtained by applying $f$ component-wise to $(f_1(i), f_2(i))$ for each $i \in s$ equals $f$ applied to the products of the multisets obtained by mapping $f_1$ and $f_2$ over $s$ respectively. That is, \[ \prod_{i \in s} f(f_1(i), f_2(i)) = f\left(\prod_{i \in s} f_1(i), \prod_{i \in s} f_2(i)\right). \]

Multiset.prod_map_mul theorem

: (m.map fun i => f i * g i).prod = (m.map f).prod * (m.map g).prod

Full source

@[to_additive (attr := simp)]
theorem prod_map_mul : (m.map fun i => f i * g i).prod = (m.map f).prod * (m.map g).prod :=
  m.prod_hom₂ (· * ·) mul_mul_mul_comm (mul_one _) _ _

Product of Pointwise Products Equals Product of Products in Multisets

Informal description

For any multiset $m$ and functions $f, g$ mapping elements of $m$ to a commutative monoid, the product of the multiset obtained by mapping each element $i \in m$ to $f(i) \cdot g(i)$ is equal to the product of the multiset obtained by mapping $f$ over $m$ multiplied by the product of the multiset obtained by mapping $g$ over $m$. That is, \[ \prod_{i \in m} (f(i) \cdot g(i)) = \left(\prod_{i \in m} f(i)\right) \cdot \left(\prod_{i \in m} g(i)\right). \]

Multiset.prod_map_pow theorem

{n : ℕ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n

Full source

@[to_additive]
theorem prod_map_pow {n : ℕ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n :=
  m.prod_hom' (powMonoidHom n : α →* α) f

Power of Multiset Product Equals Product of Powers: $(\prod f(i))^n = \prod f(i)^n$

Informal description

Let $M$ be a commutative monoid, $m$ a multiset over an index type, and $f$ a function mapping elements of $m$ to $M$. For any natural number $n$, the product of the multiset obtained by mapping each element $i \in m$ to $f(i)^n$ equals the $n$-th power of the product of the multiset obtained by mapping $f$ over $m$. That is, \[ \prod_{i \in m} f(i)^n = \left(\prod_{i \in m} f(i)\right)^n. \]

Multiset.prod_map_prod_map theorem

 (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} :
  prod (m.map fun a => prod <| n.map fun b => f a b) = prod (n.map fun b => prod <| m.map fun a => f a b)

Full source

@[to_additive]
theorem prod_map_prod_map (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} :
    prod (m.map fun a => prod <| n.map fun b => f a b) =
      prod (n.map fun b => prod <| m.map fun a => f a b) :=
  Multiset.induction_on m (by simp) fun a m ih => by simp [ih]

Double Product Commutativity for Multisets

Informal description

Let $m$ be a multiset over a type $\beta'$, $n$ a multiset over a type $\gamma$, and $f : \beta' \to \gamma \to \alpha$ a function where $\alpha$ is a commutative monoid. Then the product over $m$ of the products over $n$ of $f(a, b)$ equals the product over $n$ of the products over $m$ of $f(a, b)$. In other words, \[ \prod_{a \in m} \prod_{b \in n} f(a, b) = \prod_{b \in n} \prod_{a \in m} f(a, b). \]

Multiset.prod_dvd_prod_of_le theorem

(h : s ≤ t) : s.prod ∣ t.prod

Full source

theorem prod_dvd_prod_of_le (h : s ≤ t) : s.prod ∣ t.prod := by
  obtain ⟨z, rfl⟩ := exists_add_of_le h
  simp only [prod_add, dvd_mul_right]

Divisibility of Multiset Products Under Sub-multiset Relation

Informal description

For any two multisets $s$ and $t$ over a commutative monoid $\alpha$, if $s$ is a sub-multiset of $t$ (i.e., $s \leq t$), then the product of elements in $s$ divides the product of elements in $t$, i.e., $\prod s \mid \prod t$.

map_multiset_prod theorem

[FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f s.prod = (s.map f).prod

Full source

@[to_additive]
lemma _root_.map_multiset_prod [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) :
    f s.prod = (s.map f).prod := (s.prod_hom f).symm

Homomorphism Property for Multiset Products: $f(\prod x) = \prod f(x)$

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any multiset $s$ over $\alpha$, the image of the product of $s$ under $f$ is equal to the product of the multiset obtained by applying $f$ to each element of $s$. That is, \[ f\left(\prod_{x \in s} x\right) = \prod_{x \in s} f(x). \]

map_multiset_ne_zero_prod theorem

[FunLike F α β] [MulHomClass F α β] (f : F) {s : Multiset α} (hs : s ≠ 0) : f s.prod = (s.map f).prod

Full source

@[to_additive]
lemma _root_.map_multiset_ne_zero_prod [FunLike F α β] [MulHomClass F α β] (f : F)
    {s : Multiset α} (hs : s ≠ 0):
    f s.prod = (s.map f).prod := (s.prod_hom_ne_zero hs f).symm

Homomorphism Property for Nonempty Multiset Products: $f(\prod x) = \prod f(x)$

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplicative structures, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve multiplication. For any nonempty multiset $s$ over $\alpha$ and any homomorphism $f \in F$, the image of the product of $s$ under $f$ is equal to the product of the image of $s$ under $f$, i.e., \[ f\left(\prod_{x \in s} x\right) = \prod_{x \in s} f(x). \]

MonoidHom.map_multiset_prod theorem

(f : α →* β) (s : Multiset α) : f s.prod = (s.map f).prod

Full source

@[to_additive]
protected lemma _root_.MonoidHom.map_multiset_prod (f : α →* β) (s : Multiset α) :
    f s.prod = (s.map f).prod := (s.prod_hom f).symm

Homomorphism Property for Multiset Products: $f(\prod x) = \prod f(x)$

Informal description

Let $\alpha$ and $\beta$ be monoids, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any multiset $s$ over $\alpha$, the image of the product of $s$ under $f$ is equal to the product of the multiset obtained by applying $f$ to each element of $s$. That is, \[ f\left(\prod_{x \in s} x\right) = \prod_{x \in s} f(x). \]

MulHom.map_multiset_ne_zero_prod theorem

(f : α →ₙ* β) (s : Multiset α) (hs : s ≠ 0) : f s.prod = (s.map f).prod

Full source

@[to_additive]
protected lemma _root_.MulHom.map_multiset_ne_zero_prod (f : α →ₙ* β) (s : Multiset α)
    (hs : s ≠ 0) : f s.prod = (s.map f).prod := (s.prod_hom_ne_zero hs f).symm

Non-unital multiplicative homomorphism preserves product over nonempty multiset

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplicative structures, and let $f : \alpha \to \beta$ be a non-unital multiplicative homomorphism. For any nonempty multiset $s$ over $\alpha$, the image of the product of $s$ under $f$ is equal to the product of the image of $s$ under $f$, i.e., \[ f\left(\prod_{x \in s} x\right) = \prod_{x \in s} f(x). \]

Multiset.dvd_prod theorem

: a ∈ s → a ∣ s.prod

Full source

lemma dvd_prod : a ∈ s → a ∣ s.prod :=
  Quotient.inductionOn s (fun l a h ↦ by simpa using List.dvd_prod h) a

Element of Multiset Divides Product in Commutative Monoid

Informal description

Let $M$ be a commutative monoid and $s$ be a multiset of elements of $M$. For any element $a \in M$, if $a$ is a member of $s$ (i.e., $a \in s$), then $a$ divides the product of all elements in $s$, i.e., $a \mid \prod_{x \in s} x$.

Multiset.fst_prod theorem

(s : Multiset (α × β)) : s.prod.1 = (s.map Prod.fst).prod

Full source

@[to_additive] lemma fst_prod (s : Multiset (α × β)) : s.prod.1 = (s.map Prod.fst).prod :=
  map_multiset_prod (MonoidHom.fst _ _) _

First Component of Product Equals Product of First Components in Multiset

Informal description

Let $M$ and $N$ be commutative monoids, and let $s$ be a multiset of elements from $M \times N$. The first component of the product of $s$ equals the product of the multiset obtained by taking the first component of each element in $s$. That is, \[ \left(\prod_{(x,y) \in s} (x,y)\right)_1 = \prod_{(x,y) \in s} x. \]

Multiset.snd_prod theorem

(s : Multiset (α × β)) : s.prod.2 = (s.map Prod.snd).prod

Full source

@[to_additive] lemma snd_prod (s : Multiset (α × β)) : s.prod.2 = (s.map Prod.snd).prod :=
  map_multiset_prod (MonoidHom.snd _ _) _

Second Component of Product Equals Product of Second Components in Multiset

Informal description

Let $M$ and $N$ be commutative monoids, and let $s$ be a multiset of elements from $M \times N$. The second component of the product of all elements in $s$ equals the product of the second components of the elements in $s$. In other words, \[ \left(\prod_{(x,y) \in s} (x,y)\right)_2 = \prod_{(x,y) \in s} y. \]

Multiset.prod_dvd_prod_of_dvd theorem

 [CommMonoid β] {S : Multiset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
  (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod

Full source

theorem prod_dvd_prod_of_dvd [CommMonoid β] {S : Multiset α} (g1 g2 : α → β)
    (h : ∀ a ∈ S, g1 a ∣ g2 a) : (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod := by
  apply Multiset.induction_on' S
  · simp
  intro a T haS _ IH
  simp [mul_dvd_mul (h a haS) IH]

Divisibility of Multiset Products under Pointwise Divisibility

Informal description

Let $S$ be a multiset over a type $\alpha$, and let $g_1, g_2 : \alpha \to \beta$ be functions into a commutative monoid $\beta$. If for every element $a \in S$, $g_1(a)$ divides $g_2(a)$, then the product of the image of $S$ under $g_1$ divides the product of the image of $S$ under $g_2$.

Multiset.sumAddMonoidHom definition

: Multiset α →+ α

Full source

/-- `Multiset.sum`, the sum of the elements of a multiset, promoted to a morphism of
`AddCommMonoid`s. -/
def sumAddMonoidHom : MultisetMultiset α →+ α where
  toFun := sum
  map_zero' := sum_zero
  map_add' := sum_add

Additive monoid homomorphism of multiset sum

Informal description

The function `Multiset.sumAddMonoidHom` is the additive monoid homomorphism that maps a multiset to the sum of its elements. It satisfies: 1. $f(0) = 0$ (preservation of zero) 2. $f(s + t) = f(s) + f(t)$ for all multisets $s, t$ (preservation of addition) Here, the sum of a multiset is defined as the sum of all its elements (counting multiplicities) in the additive commutative monoid $\alpha$.

Multiset.coe_sumAddMonoidHom theorem

: (sumAddMonoidHom : Multiset α → α) = sum

Full source

@[simp]
theorem coe_sumAddMonoidHom : (sumAddMonoidHom : Multiset α → α) = sum :=
  rfl

Sum Homomorphism Equals Sum Function on Multisets

Informal description

The additive monoid homomorphism `sumAddMonoidHom` from multisets over a type $\alpha$ to $\alpha$ itself is equal to the sum function, which computes the sum of all elements in a multiset (counting multiplicities).

Multiset.prod_map_inv' theorem

(m : Multiset α) : (m.map Inv.inv).prod = m.prod⁻¹

Full source

@[to_additive]
theorem prod_map_inv' (m : Multiset α) : (m.map Inv.inv).prod = m.prod⁻¹ :=
  m.prod_hom (invMonoidHom : α →* α)

Inversion Commutes with Multiset Product: $\prod x^{-1} = (\prod x)^{-1}$

Informal description

For any multiset $m$ over a commutative division monoid $\alpha$, the product of the multiset obtained by mapping the inversion operation over $m$ is equal to the inverse of the product of $m$. That is, \[ \prod_{x \in m} x^{-1} = \left(\prod_{x \in m} x\right)^{-1}. \]

Multiset.prod_map_inv theorem

: (m.map fun i => (f i)⁻¹).prod = (m.map f).prod⁻¹

Full source

@[to_additive (attr := simp)]
theorem prod_map_inv : (m.map fun i => (f i)⁻¹).prod = (m.map f).prod⁻¹ := by
  rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]

Inversion Commutes with Multiset Product under Mapping: $\prod (f i)^{-1} = (\prod f i)^{-1}$

Informal description

For any multiset $m$ over a type $\iota$ and any function $f : \iota \to G$ where $G$ is a commutative division monoid, the product of the multiset obtained by mapping $\lambda i, (f i)^{-1}$ over $m$ equals the inverse of the product of the multiset obtained by mapping $f$ over $m$. That is, \[ \prod_{i \in m} (f i)^{-1} = \left(\prod_{i \in m} f i\right)^{-1}. \]

Multiset.prod_map_div theorem

: (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map g).prod

Full source

@[to_additive (attr := simp)]
theorem prod_map_div : (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map g).prod :=
  m.prod_hom₂ (· / ·) mul_div_mul_comm (div_one _) _ _

Product of Quotients Equals Quotient of Products in Multisets

Informal description

For any multiset $m$ over a type $\iota$ and functions $f, g : \iota \to G$ where $G$ is a division commutative monoid, the product of the multiset obtained by mapping $\lambda i, f(i) / g(i)$ over $m$ equals the division of the product of the multiset obtained by mapping $f$ over $m$ by the product of the multiset obtained by mapping $g$ over $m$. That is, \[ \prod_{i \in m} \left(\frac{f(i)}{g(i)}\right) = \frac{\prod_{i \in m} f(i)}{\prod_{i \in m} g(i)}. \]

Multiset.prod_map_zpow theorem

{n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n

Full source

@[to_additive]
theorem prod_map_zpow {n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n := by
  convert (m.map f).prod_hom (zpowGroupHom n : α →* α)
  simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

Power of Product Equals Product of Powers in Multisets: $\prod f(i)^n = (\prod f(i))^n$

Informal description

For any multiset $m$ over a type $\iota$, any function $f : \iota \to G$ where $G$ is a division commutative monoid, and any integer $n$, the product of the multiset obtained by mapping $\lambda i, f(i)^n$ over $m$ equals the $n$-th power of the product of the multiset obtained by mapping $f$ over $m$. That is, \[ \prod_{i \in m} f(i)^n = \left(\prod_{i \in m} f(i)\right)^n. \]

Multiset.sum_map_singleton theorem

(s : Multiset α) : (s.map fun a => ({ a } : Multiset α)).sum = s

Full source

@[simp]
theorem sum_map_singleton (s : Multiset α) : (s.map fun a => ({a} : Multiset α)).sum = s :=
  Multiset.induction_on s (by simp) (by simp)

Sum of Singletons Equals Original Multiset

Informal description

For any multiset $s$ over a type $\alpha$, the sum of the singleton multisets $\{a\}$ for each element $a \in s$ is equal to $s$ itself.

Multiset.sum_nat_mod theorem

(s : Multiset ℕ) (n : ℕ) : s.sum % n = (s.map (· % n)).sum % n

Full source

theorem sum_nat_mod (s : Multiset ℕ) (n : ℕ) : s.sum % n = (s.map (· % n)).sum % n := by
  induction s using Multiset.induction <;> simp [Nat.add_mod, *]

Modular Sum Property for Multisets of Natural Numbers

Informal description

For any multiset $s$ of natural numbers and any natural number $n$, the sum of all elements in $s$ modulo $n$ is equal to the sum of the elements in $s$ modulo $n$ (where each element is first taken modulo $n$). That is: $$ \left(\sum_{x \in s} x\right) \bmod n = \left(\sum_{x \in s} (x \bmod n)\right) \bmod n $$

Multiset.prod_nat_mod theorem

(s : Multiset ℕ) (n : ℕ) : s.prod % n = (s.map (· % n)).prod % n

Full source

theorem prod_nat_mod (s : Multiset ℕ) (n : ℕ) : s.prod % n = (s.map (· % n)).prod % n := by
  induction s using Multiset.induction <;> simp [Nat.mul_mod, *]

Modular Product Property for Multisets of Natural Numbers

Informal description

For any multiset $s$ of natural numbers and any natural number $n$, the remainder of the product of all elements in $s$ modulo $n$ is equal to the remainder of the product of all elements in $s$ modulo $n$ (where each element is first taken modulo $n$).

Multiset.sum_int_mod theorem

(s : Multiset ℤ) (n : ℤ) : s.sum % n = (s.map (· % n)).sum % n

Full source

theorem sum_int_mod (s : Multiset ℤ) (n : ℤ) : s.sum % n = (s.map (· % n)).sum % n := by
  induction s using Multiset.induction <;> simp [Int.add_emod, *]

Modular Sum Property for Multisets of Integers

Informal description

For any multiset $s$ of integers and any integer $n$, the remainder of the sum of all elements in $s$ modulo $n$ is equal to the remainder of the sum of all elements in $s$ modulo $n$ (where each element is first taken modulo $n$). That is: $$ \left(\sum_{x \in s} x\right) \bmod n = \left(\sum_{x \in s} (x \bmod n)\right) \bmod n $$

Multiset.prod_int_mod theorem

(s : Multiset ℤ) (n : ℤ) : s.prod % n = (s.map (· % n)).prod % n

Full source

theorem prod_int_mod (s : Multiset ℤ) (n : ℤ) : s.prod % n = (s.map (· % n)).prod % n := by
  induction s using Multiset.induction <;> simp [Int.mul_emod, *]

Modular Product Property for Multisets of Integers

Informal description

For any multiset $s$ of integers and any integer $n$, the remainder of the product of all elements in $s$ modulo $n$ is equal to the remainder of the product of all elements in $s$ modulo $n$ (where each element is first taken modulo $n$). That is: $$ \left(\prod_{x \in s} x\right) \bmod n = \left(\prod_{x \in s} (x \bmod n)\right) \bmod n $$

Multiset.sum_map_tsub theorem

 [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (· + ·) (· ≤ ·)]
  [ContravariantClass α α (· + ·) (· ≤ ·)] [Sub α] [OrderedSub α] (l : Multiset ι) {f g : ι → α}
  (hfg : ∀ x ∈ l, g x ≤ f x) : (l.map fun x ↦ f x - g x).sum = (l.map f).sum - (l.map g).sum

Full source

theorem sum_map_tsub [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α]
    [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)] [Sub α]
    [OrderedSub α] (l : Multiset ι) {f g : ι → α} (hfg : ∀ x ∈ l, g x ≤ f x) :
    (l.map fun x ↦ f x - g x).sum = (l.map f).sum - (l.map g).sum :=
  eq_tsub_of_add_eq <| by
    rw [← sum_map_add]
    congr 1
    exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

Sum of Differences Equals Difference of Sums for Multisets

Informal description

Let $\alpha$ be an additive commutative monoid with a partial order and a subtraction operation satisfying the ordered subtraction property. For any multiset $l$ over a type $\iota$ and functions $f, g : \iota \to \alpha$ such that $g(x) \leq f(x)$ for all $x \in l$, the sum of the differences $f(x) - g(x)$ over $l$ equals the difference of the sums: \[ \sum_{x \in l} (f(x) - g(x)) = \left(\sum_{x \in l} f(x)\right) - \left(\sum_{x \in l} g(x)\right). \]

Main declarations