mathlib3 documentation

algebra.big_operators.multiset.basic

Sums and products over multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define products and sums indexed by multisets. This is later used to define products and sums indexed by finite sets.

Main declarations #

Implementation notes #

Nov 2022: To speed the Lean 4 port, lemmas requiring extra algebra imports (data.list.big_operators.lemmas rather than .basic) have been moved to a separate file, algebra.big_operators.multiset.lemmas. This split does not need to be permanent.

source
def multiset.sum {α : Type u_2} [add_comm_monoid α] :
multiset α → α

Sum of a multiset given a commutative additive monoid structure on α. sum {a, b, c} = a + b + c

Equations
source
def multiset.prod {α : Type u_2} [comm_monoid α] :
multiset α → α

Product of a multiset given a commutative monoid structure on α. prod {a, b, c} = a * b * c

Equations
source
theorem multiset.sum_eq_foldr {α : Type u_2} [add_comm_monoid α] (s : multiset α) :
s.sum = multiset.foldr has_add.add _ 0 s
source
theorem multiset.prod_eq_foldr {α : Type u_2} [comm_monoid α] (s : multiset α) :
s.prod = multiset.foldr has_mul.mul _ 1 s
source
theorem multiset.prod_eq_foldl {α : Type u_2} [comm_monoid α] (s : multiset α) :
s.prod = multiset.foldl has_mul.mul _ 1 s
source
theorem multiset.sum_eq_foldl {α : Type u_2} [add_comm_monoid α] (s : multiset α) :
s.sum = multiset.foldl has_add.add _ 0 s
source
@[simp, norm_cast]
theorem multiset.coe_sum {α : Type u_2} [add_comm_monoid α] (l : list α) :
↑l.sum = l.sum
source
@[simp, norm_cast]
theorem multiset.coe_prod {α : Type u_2} [comm_monoid α] (l : list α) :
↑l.prod = l.prod
source
@[simp]
theorem multiset.sum_to_list {α : Type u_2} [add_comm_monoid α] (s : multiset α) :
s.to_list.sum = s.sum
source
@[simp]
theorem multiset.prod_to_list {α : Type u_2} [comm_monoid α] (s : multiset α) :
s.to_list.prod = s.prod
source
@[simp]
theorem multiset.prod_zero {α : Type u_2} [comm_monoid α] :
0.prod = 1
source
@[simp]
theorem multiset.sum_zero {α : Type u_2} [add_comm_monoid α] :
0.sum = 0
source
@[simp]
theorem multiset.prod_cons {α : Type u_2} [comm_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).prod = a * s.prod
source
@[simp]
theorem multiset.sum_cons {α : Type u_2} [add_comm_monoid α] (a : α) (s : multiset α) :
(a ::ₘ s).sum = a + s.sum
source
@[simp]
theorem multiset.prod_erase {α : Type u_2} [comm_monoid α] {s : multiset α} {a : α} [decidable_eq α] (h : a ∈ s) :
a * (s.erase a).prod = s.prod
source
@[simp]
theorem multiset.sum_erase {α : Type u_2} [add_comm_monoid α] {s : multiset α} {a : α} [decidable_eq α] (h : a ∈ s) :
a + (s.erase a).sum = s.sum
source
@[simp]
theorem multiset.sum_map_erase {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {m : multiset ι} {f : ι → α} [decidable_eq ι] {a : ι} (h : a ∈ m) :
f a + (multiset.map f (m.erase a)).sum = (multiset.map f m).sum
source
@[simp]
theorem multiset.prod_map_erase {ι : Type u_1} {α : Type u_2} [comm_monoid α] {m : multiset ι} {f : ι → α} [decidable_eq ι] {a : ι} (h : a ∈ m) :
f a * (multiset.map f (m.erase a)).prod = (multiset.map f m).prod
source
@[simp]
theorem multiset.prod_singleton {α : Type u_2} [comm_monoid α] (a : α) :
{a}.prod = a
source
@[simp]
theorem multiset.sum_singleton {α : Type u_2} [add_comm_monoid α] (a : α) :
{a}.sum = a
source
theorem multiset.prod_pair {α : Type u_2} [comm_monoid α] (a b : α) :
{a, b}.prod = a * b
source
theorem multiset.sum_pair {α : Type u_2} [add_comm_monoid α] (a b : α) :
{a, b}.sum = a + b
source
@[simp]
theorem multiset.prod_add {α : Type u_2} [comm_monoid α] (s t : multiset α) :
(s + t).prod = s.prod * t.prod
source
@[simp]
theorem multiset.sum_add {α : Type u_2} [add_comm_monoid α] (s t : multiset α) :
(s + t).sum = s.sum + t.sum
source
theorem multiset.prod_nsmul {α : Type u_2} [comm_monoid α] (m : multiset α) (n : ℕ) :
(n • m).prod = m.prod ^ n
source
@[simp]
theorem multiset.prod_replicate {α : Type u_2} [comm_monoid α] (n : ℕ) (a : α) :
(multiset.replicate n a).prod = a ^ n
source
@[simp]
theorem multiset.sum_replicate {α : Type u_2} [add_comm_monoid α] (n : ℕ) (a : α) :
(multiset.replicate n a).sum = n • a
source
theorem multiset.prod_map_eq_pow_single {ι : Type u_1} {α : Type u_2} [comm_monoid α] {m : multiset ι} {f : ι → α} [decidable_eq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1) :
(multiset.map f m).prod = f i ^ multiset.count i m
source
theorem multiset.sum_map_eq_nsmul_single {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {m : multiset ι} {f : ι → α} [decidable_eq ι] (i : ι) (hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0) :
(multiset.map f m).sum = multiset.count i m • f i
source
theorem multiset.sum_eq_nsmul_single {α : Type u_2} [add_comm_monoid α] {s : multiset α} [decidable_eq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0) :
s.sum = multiset.count a s • a
source
theorem multiset.prod_eq_pow_single {α : Type u_2} [comm_monoid α] {s : multiset α} [decidable_eq α] (a : α) (h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1) :
s.prod = a ^ multiset.count a s
source
theorem multiset.pow_count {α : Type u_2} [comm_monoid α] {s : multiset α} [decidable_eq α] (a : α) :
a ^ multiset.count a s = (multiset.filter (eq a) s).prod
source
theorem multiset.nsmul_count {α : Type u_2} [add_comm_monoid α] {s : multiset α} [decidable_eq α] (a : α) :
multiset.count a s • a = (multiset.filter (eq a) s).sum
source
theorem multiset.sum_hom {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] (s : multiset α) {F : Type u_1} [add_monoid_hom_class F α β] (f : F) :
(multiset.map ⇑f s).sum = ⇑f s.sum
source
theorem multiset.prod_hom {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (s : multiset α) {F : Type u_1} [monoid_hom_class F α β] (f : F) :
(multiset.map ⇑f s).prod = ⇑f s.prod
source
theorem multiset.sum_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] (s : multiset ι) {F : Type u_4} [add_monoid_hom_class F α β] (f : F) (g : ι → α) :
(multiset.map (λ (i : ι), ⇑f (g i)) s).sum = ⇑f (multiset.map g s).sum
source
theorem multiset.prod_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (s : multiset ι) {F : Type u_4} [monoid_hom_class F α β] (f : F) (g : ι → α) :
(multiset.map (λ (i : ι), ⇑f (g i)) s).prod = ⇑f (multiset.map g s).prod
source
theorem multiset.prod_hom₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] (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₂ : ι → β) :
(multiset.map (λ (i : ι), f (f₁ i) (f₂ i)) s).prod = f (multiset.map f₁ s).prod (multiset.map f₂ s).prod
source
theorem multiset.sum_hom₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] (s : multiset ι) (f : α → β → γ) (hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d) (hf' : f 0 0 = 0) (f₁ : ι → α) (f₂ : ι → β) :
(multiset.map (λ (i : ι), f (f₁ i) (f₂ i)) s).sum = f (multiset.map f₁ s).sum (multiset.map f₂ s).sum
source
theorem multiset.sum_hom_rel {ι : Type u_1} {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] (s : multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c)) :
r (multiset.map f s).sum (multiset.map g s).sum
source
theorem multiset.prod_hom_rel {ι : Type u_1} {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (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 (multiset.map f s).prod (multiset.map g s).prod
source
theorem multiset.sum_map_zero {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {m : multiset ι} :
(multiset.map (λ (i : ι), 0) m).sum = 0
source
theorem multiset.prod_map_one {ι : Type u_1} {α : Type u_2} [comm_monoid α] {m : multiset ι} :
(multiset.map (λ (i : ι), 1) m).prod = 1
source
@[simp]
theorem multiset.sum_map_add {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {m : multiset ι} {f g : ι → α} :
(multiset.map (λ (i : ι), f i + g i) m).sum = (multiset.map f m).sum + (multiset.map g m).sum
source
@[simp]
theorem multiset.prod_map_mul {ι : Type u_1} {α : Type u_2} [comm_monoid α] {m : multiset ι} {f g : ι → α} :
(multiset.map (λ (i : ι), f i * g i) m).prod = (multiset.map f m).prod * (multiset.map g m).prod
source
@[simp]
theorem multiset.prod_map_neg {α : Type u_2} [comm_monoid α] [has_distrib_neg α] (s : multiset α) :
(multiset.map has_neg.neg s).prod = (-1) ^ ⇑multiset.card s * s.prod
source
theorem multiset.prod_map_pow {ι : Type u_1} {α : Type u_2} [comm_monoid α] {m : multiset ι} {f : ι → α} {n : ℕ} :
(multiset.map (λ (i : ι), f i ^ n) m).prod = (multiset.map f m).prod ^ n
source
theorem multiset.sum_map_nsmul {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {m : multiset ι} {f : ι → α} {n : ℕ} :
(multiset.map (λ (i : ι), n • f i) m).sum = n • (multiset.map f m).sum
source
theorem multiset.prod_map_prod_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] (m : multiset β) (n : multiset γ) {f : β → γ → α} :
(multiset.map (λ (a : β), (multiset.map (λ (b : γ), f a b) n).prod) m).prod = (multiset.map (λ (b : γ), (multiset.map (λ (a : β), f a b) m).prod) n).prod
source
theorem multiset.sum_map_sum_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] (m : multiset β) (n : multiset γ) {f : β → γ → α} :
(multiset.map (λ (a : β), (multiset.map (λ (b : γ), f a b) n).sum) m).sum = (multiset.map (λ (b : γ), (multiset.map (λ (a : β), f a b) m).sum) n).sum
source
theorem multiset.prod_induction {α : Type u_2} [comm_monoid α] (p : α → Prop) (s : multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ (a : α), a ∈ s → p a) :
p s.prod
source
theorem multiset.sum_induction {α : Type u_2} [add_comm_monoid α] (p : α → Prop) (s : multiset α) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (p_one : p 0) (p_s : ∀ (a : α), a ∈ s → p a) :
p s.sum
source
theorem multiset.sum_induction_nonempty {α : Type u_2} [add_comm_monoid α] {s : multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a + b)) (hs : s ≠ ∅) (p_s : ∀ (a : α), a ∈ s → p a) :
p s.sum
source
theorem multiset.prod_induction_nonempty {α : Type u_2} [comm_monoid α] {s : multiset α} (p : α → Prop) (p_mul : ∀ (a b : α), p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ (a : α), a ∈ s → p a) :
p s.prod
source
theorem multiset.prod_dvd_prod_of_le {α : Type u_2} [comm_monoid α] {s t : multiset α} (h : s ≤ t) :
s.prod ∣ t.prod
source
theorem multiset.prod_dvd_prod_of_dvd {α : Type u_2} {β : Type u_3} [comm_monoid β] {S : multiset α} (g1 g2 : α → β) (h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a) :
(multiset.map g1 S).prod ∣ (multiset.map g2 S).prod
source
def multiset.sum_add_monoid_hom {α : Type u_2} [add_comm_monoid α] :
multiset α →+ α

multiset.sum, the sum of the elements of a multiset, promoted to a morphism of add_comm_monoids.

Equations
source
@[simp]
theorem multiset.coe_sum_add_monoid_hom {α : Type u_2} [add_comm_monoid α] :
⇑multiset.sum_add_monoid_hom = multiset.sum
source
theorem multiset.prod_eq_zero {α : Type u_2} [comm_monoid_with_zero α] {s : multiset α} (h : 0 ∈ s) :
s.prod = 0
source
theorem multiset.prod_eq_zero_iff {α : Type u_2} [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] {s : multiset α} :
s.prod = 0 ↔ 0 ∈ s
source
theorem multiset.prod_ne_zero {α : Type u_2} [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] {s : multiset α} (h : 0 ∉ s) :
s.prod ≠ 0
source
theorem multiset.sum_map_neg' {α : Type u_2} [subtraction_comm_monoid α] (m : multiset α) :
(multiset.map has_neg.neg m).sum = -m.sum
source
theorem multiset.prod_map_inv' {α : Type u_2} [division_comm_monoid α] (m : multiset α) :
(multiset.map has_inv.inv m).prod = (m.prod)⁻¹
source
@[simp]
theorem multiset.sum_map_neg {ι : Type u_1} {α : Type u_2} [subtraction_comm_monoid α] {m : multiset ι} {f : ι → α} :
(multiset.map (λ (i : ι), -f i) m).sum = -(multiset.map f m).sum
source
@[simp]
theorem multiset.prod_map_inv {ι : Type u_1} {α : Type u_2} [division_comm_monoid α] {m : multiset ι} {f : ι → α} :
(multiset.map (λ (i : ι), (f i)⁻¹) m).prod = ((multiset.map f m).prod)⁻¹
source
@[simp]
theorem multiset.sum_map_sub {ι : Type u_1} {α : Type u_2} [subtraction_comm_monoid α] {m : multiset ι} {f g : ι → α} :
(multiset.map (λ (i : ι), f i - g i) m).sum = (multiset.map f m).sum - (multiset.map g m).sum
source
@[simp]
theorem multiset.prod_map_div {ι : Type u_1} {α : Type u_2} [division_comm_monoid α] {m : multiset ι} {f g : ι → α} :
(multiset.map (λ (i : ι), f i / g i) m).prod = (multiset.map f m).prod / (multiset.map g m).prod
source
theorem multiset.prod_map_zpow {ι : Type u_1} {α : Type u_2} [division_comm_monoid α] {m : multiset ι} {f : ι → α} {n : ℤ} :
(multiset.map (λ (i : ι), f i ^ n) m).prod = (multiset.map f m).prod ^ n
source
theorem multiset.sum_map_zsmul {ι : Type u_1} {α : Type u_2} [subtraction_comm_monoid α] {m : multiset ι} {f : ι → α} {n : ℤ} :
(multiset.map (λ (i : ι), n • f i) m).sum = n • (multiset.map f m).sum
source
theorem multiset.sum_map_mul_left {ι : Type u_1} {α : Type u_2} [non_unital_non_assoc_semiring α] {a : α} {s : multiset ι} {f : ι → α} :
(multiset.map (λ (i : ι), a * f i) s).sum = a * (multiset.map f s).sum
source
theorem multiset.sum_map_mul_right {ι : Type u_1} {α : Type u_2} [non_unital_non_assoc_semiring α] {a : α} {s : multiset ι} {f : ι → α} :
(multiset.map (λ (i : ι), f i * a) s).sum = (multiset.map f s).sum * a
source
theorem multiset.dvd_sum {α : Type u_2} [semiring α] {a : α} {s : multiset α} :
(∀ (x : α), x ∈ s → a ∣ x) → a ∣ s.sum

Order #

source
theorem multiset.sum_nonneg {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 0 ≤ x) → 0 ≤ s.sum
source
theorem multiset.one_le_prod_of_one_le {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 1 ≤ x) → 1 ≤ s.prod
source
theorem multiset.single_le_prod {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 1 ≤ x) → ∀ (x : α), x ∈ s → x ≤ s.prod
source
theorem multiset.single_le_sum {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 0 ≤ x) → ∀ (x : α), x ∈ s → x ≤ s.sum
source
theorem multiset.prod_le_pow_card {α : Type u_2} [ordered_comm_monoid α] (s : multiset α) (n : α) (h : ∀ (x : α), x ∈ s → x ≤ n) :
s.prod ≤ n ^ ⇑multiset.card s
source
theorem multiset.sum_le_card_nsmul {α : Type u_2} [ordered_add_comm_monoid α] (s : multiset α) (n : α) (h : ∀ (x : α), x ∈ s → x ≤ n) :
s.sum ≤ ⇑multiset.card s • n
source
theorem multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 1 ≤ x) → s.prod = 1 → ∀ (x : α), x ∈ s → x = 1
source
theorem multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} :
(∀ (x : α), x ∈ s → 0 ≤ x) → s.sum = 0 → ∀ (x : α), x ∈ s → x = 0
source
theorem multiset.sum_le_sum_of_rel_le {α : Type u_2} [ordered_add_comm_monoid α] {s t : multiset α} (h : multiset.rel has_le.le s t) :
s.sum ≤ t.sum
source
theorem multiset.prod_le_prod_of_rel_le {α : Type u_2} [ordered_comm_monoid α] {s t : multiset α} (h : multiset.rel has_le.le s t) :
s.prod ≤ t.prod
source
theorem multiset.prod_map_le_prod_map {ι : Type u_1} {α : Type u_2} [ordered_comm_monoid α] {s : multiset ι} (f g : ι → α) (h : ∀ (i : ι), i ∈ s → f i ≤ g i) :
(multiset.map f s).prod ≤ (multiset.map g s).prod
source
theorem multiset.sum_map_le_sum_map {ι : Type u_1} {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset ι} (f g : ι → α) (h : ∀ (i : ι), i ∈ s → f i ≤ g i) :
(multiset.map f s).sum ≤ (multiset.map g s).sum
source
theorem multiset.prod_map_le_prod {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} (f : α → α) (h : ∀ (x : α), x ∈ s → f x ≤ x) :
(multiset.map f s).prod ≤ s.prod
source
theorem multiset.sum_map_le_sum {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} (f : α → α) (h : ∀ (x : α), x ∈ s → f x ≤ x) :
(multiset.map f s).sum ≤ s.sum
source
theorem multiset.sum_le_sum_map {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} (f : α → α) (h : ∀ (x : α), x ∈ s → x ≤ f x) :
s.sum ≤ (multiset.map f s).sum
source
theorem multiset.prod_le_prod_map {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} (f : α → α) (h : ∀ (x : α), x ∈ s → x ≤ f x) :
s.prod ≤ (multiset.map f s).prod
source
theorem multiset.card_nsmul_le_sum {α : Type u_2} [ordered_add_comm_monoid α] {s : multiset α} {a : α} (h : ∀ (x : α), x ∈ s → a ≤ x) :
⇑multiset.card s • a ≤ s.sum
source
theorem multiset.pow_card_le_prod {α : Type u_2} [ordered_comm_monoid α] {s : multiset α} {a : α} (h : ∀ (x : α), x ∈ s → a ≤ x) :
a ^ ⇑multiset.card s ≤ s.prod
source
theorem multiset.prod_nonneg {α : Type u_2} [ordered_comm_semiring α] {m : multiset α} (h : ∀ (a : α), a ∈ m → 0 ≤ a) :
0 ≤ m.prod
source
theorem multiset.prod_eq_one {α : Type u_2} [comm_monoid α] {m : multiset α} (h : ∀ (x : α), x ∈ m → x = 1) :
m.prod = 1

Slightly more general version of multiset.prod_eq_one_iff for a non-ordered monoid

source
theorem multiset.sum_eq_zero {α : Type u_2} [add_comm_monoid α] {m : multiset α} (h : ∀ (x : α), x ∈ m → x = 0) :
m.sum = 0

Slightly more general version of multiset.sum_eq_zero_iff for a non-ordered add_monoid

source
theorem multiset.le_sum_of_mem {α : Type u_2} [canonically_ordered_add_monoid α] {m : multiset α} {a : α} (h : a ∈ m) :
a ≤ m.sum
source
theorem multiset.le_prod_of_mem {α : Type u_2} [canonically_ordered_monoid α] {m : multiset α} {a : α} (h : a ∈ m) :
a ≤ m.prod
source
theorem multiset.le_sum_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (p : α → Prop) (h_one : f 0 = 0) (hp_one : p 0) (h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_mul : ∀ (a b : α), p a → p b → p (a + b)) (s : multiset α) (hps : ∀ (a : α), a ∈ s → p a) :
f s.sum ≤ (multiset.map f s).sum
source
theorem multiset.le_prod_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [comm_monoid α] [ordered_comm_monoid β] (f : α → β) (p : α → Prop) (h_one : f 1 = 1) (hp_one : p 1) (h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ (a b : α), p a → p b → p (a * b)) (s : multiset α) (hps : ∀ (a : α), a ∈ s → p a) :
f s.prod ≤ (multiset.map f s).prod
source
theorem multiset.le_prod_of_submultiplicative {α : Type u_2} {β : Type u_3} [comm_monoid α] [ordered_comm_monoid β] (f : α → β) (h_one : f 1 = 1) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (s : multiset α) :
f s.prod ≤ (multiset.map f s).prod
source
theorem multiset.le_sum_of_subadditive {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (h_one : f 0 = 0) (h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : multiset α) :
f s.sum ≤ (multiset.map f s).sum
source
theorem multiset.le_prod_nonempty_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [comm_monoid α] [ordered_comm_monoid β] (f : α → β) (p : α → Prop) (h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ (a b : α), p a → p b → p (a * b)) (s : multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ (a : α), a ∈ s → p a) :
f s.prod ≤ (multiset.map f s).prod
source
theorem multiset.le_sum_nonempty_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (p : α → Prop) (h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_mul : ∀ (a b : α), p a → p b → p (a + b)) (s : multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ (a : α), a ∈ s → p a) :
f s.sum ≤ (multiset.map f s).sum
source
theorem multiset.le_sum_nonempty_of_subadditive {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [ordered_add_comm_monoid β] (f : α → β) (h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : multiset α) (hs_nonempty : s ≠ ∅) :
f s.sum ≤ (multiset.map f s).sum
source
theorem multiset.le_prod_nonempty_of_submultiplicative {α : Type u_2} {β : Type u_3} [comm_monoid α] [ordered_comm_monoid β] (f : α → β) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (s : multiset α) (hs_nonempty : s ≠ ∅) :
f s.prod ≤ (multiset.map f s).prod
source
@[simp]
theorem multiset.sum_map_singleton {α : Type u_2} (s : multiset α) :
(multiset.map (λ (a : α), {a}) s).sum = s
source
theorem multiset.abs_sum_le_sum_abs {α : Type u_2} [linear_ordered_add_comm_group α] {s : multiset α} :
|s.sum| ≤ (multiset.map has_abs.abs s).sum
source
theorem multiset.sum_nat_mod (s : multiset ℕ) (n : ℕ) :
s.sum % n = (multiset.map (λ (_x : ℕ), _x % n) s).sum % n
source
theorem multiset.prod_nat_mod (s : multiset ℕ) (n : ℕ) :
s.prod % n = (multiset.map (λ (_x : ℕ), _x % n) s).prod % n
source
theorem multiset.sum_int_mod (s : multiset ℤ) (n : ℤ) :
s.sum % n = (multiset.map (λ (_x : ℤ), _x % n) s).sum % n
source
theorem multiset.prod_int_mod (s : multiset ℤ) (n : ℤ) :
s.prod % n = (multiset.map (λ (_x : ℤ), _x % n) s).prod % n
source
theorem map_multiset_prod {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {F : Type u_1} [monoid_hom_class F α β] (f : F) (s : multiset α) :
⇑f s.prod = (multiset.map ⇑f s).prod
source
theorem map_multiset_sum {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {F : Type u_1} [add_monoid_hom_class F α β] (f : F) (s : multiset α) :
⇑f s.sum = (multiset.map ⇑f s).sum
source
@[protected]
theorem monoid_hom.map_multiset_prod {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (f : α →* β) (s : multiset α) :
⇑f s.prod = (multiset.map ⇑f s).prod
source
@[protected]
theorem add_monoid_hom.map_multiset_sum {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] (f : α →+ β) (s : multiset α) :
⇑f s.sum = (multiset.map ⇑f s).sum