Documentation

Mathlib.Algebra.BigOperators.Multiset.Basic

Sums and products over multisets #

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.

theorem Multiset.sum.proof_1 {α : Type u_1} [AddCommMonoid α] (x : α) (y : α) (z : α) :
x + (y + z) = y + (x + z)
def Multiset.sum {α : Type u_2} [AddCommMonoid α] :
Multiset αα

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

Equations
Instances For
    def Multiset.prod {α : Type u_2} [CommMonoid α] :
    Multiset αα

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

    Equations
    Instances For
      theorem Multiset.sum_eq_foldr {α : Type u_2} [AddCommMonoid α] (s : Multiset α) :
      Multiset.sum s = Multiset.foldr (fun (x x_1 : α) => x + x_1) 0 s
      theorem Multiset.prod_eq_foldr {α : Type u_2} [CommMonoid α] (s : Multiset α) :
      Multiset.prod s = Multiset.foldr (fun (x x_1 : α) => x * x_1) 1 s
      theorem Multiset.sum_eq_foldl {α : Type u_2} [AddCommMonoid α] (s : Multiset α) :
      Multiset.sum s = Multiset.foldl (fun (x x_1 : α) => x + x_1) 0 s
      theorem Multiset.prod_eq_foldl {α : Type u_2} [CommMonoid α] (s : Multiset α) :
      Multiset.prod s = Multiset.foldl (fun (x x_1 : α) => x * x_1) 1 s
      @[simp]
      theorem Multiset.sum_coe {α : Type u_2} [AddCommMonoid α] (l : List α) :
      @[simp]
      theorem Multiset.prod_coe {α : Type u_2} [CommMonoid α] (l : List α) :
      @[simp]
      theorem Multiset.sum_zero {α : Type u_2} [AddCommMonoid α] :
      @[simp]
      theorem Multiset.prod_zero {α : Type u_2} [CommMonoid α] :
      @[simp]
      theorem Multiset.sum_cons {α : Type u_2} [AddCommMonoid α] (a : α) (s : Multiset α) :
      @[simp]
      theorem Multiset.prod_cons {α : Type u_2} [CommMonoid α] (a : α) (s : Multiset α) :
      @[simp]
      theorem Multiset.sum_erase {α : Type u_2} [AddCommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a s) :
      @[simp]
      theorem Multiset.prod_erase {α : Type u_2} [CommMonoid α] {s : Multiset α} {a : α} [DecidableEq α] (h : a s) :
      @[simp]
      theorem Multiset.sum_map_erase {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ια} [DecidableEq ι] {a : ι} (h : a m) :
      @[simp]
      theorem Multiset.prod_map_erase {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ια} [DecidableEq ι] {a : ι} (h : a m) :
      @[simp]
      theorem Multiset.sum_singleton {α : Type u_2} [AddCommMonoid α] (a : α) :
      @[simp]
      theorem Multiset.prod_singleton {α : Type u_2} [CommMonoid α] (a : α) :
      theorem Multiset.sum_pair {α : Type u_2} [AddCommMonoid α] (a : α) (b : α) :
      Multiset.sum {a, b} = a + b
      theorem Multiset.prod_pair {α : Type u_2} [CommMonoid α] (a : α) (b : α) :
      Multiset.prod {a, b} = a * b
      @[simp]
      theorem Multiset.sum_add {α : Type u_2} [AddCommMonoid α] (s : Multiset α) (t : Multiset α) :
      @[simp]
      theorem Multiset.prod_add {α : Type u_2} [CommMonoid α] (s : Multiset α) (t : Multiset α) :
      theorem Multiset.sum_nsmul {α : Type u_2} [AddCommMonoid α] (m : Multiset α) (n : ) :
      abbrev Multiset.sum_nsmul.match_1 (motive : Prop) :
      ∀ (x : ), (Unitmotive 0)(∀ (n : ), motive (Nat.succ n))motive x
      Equations
      • =
      Instances For
        theorem Multiset.prod_nsmul {α : Type u_2} [CommMonoid α] (m : Multiset α) (n : ) :
        @[simp]
        theorem Multiset.sum_replicate {α : Type u_2} [AddCommMonoid α] (n : ) (a : α) :
        @[simp]
        theorem Multiset.prod_replicate {α : Type u_2} [CommMonoid α] (n : ) (a : α) :
        theorem Multiset.sum_map_eq_nsmul_single {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ια} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ii' mf i' = 0) :
        theorem Multiset.prod_map_eq_pow_single {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ια} [DecidableEq ι] (i : ι) (hf : ∀ (i' : ι), i' ii' mf i' = 1) :
        theorem Multiset.sum_eq_nsmul_single {α : Type u_2} [AddCommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' aa' sa' = 0) :
        theorem Multiset.prod_eq_pow_single {α : Type u_2} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) (h : ∀ (a' : α), a' aa' sa' = 1) :
        theorem Multiset.pow_count {α : Type u_2} [CommMonoid α] {s : Multiset α} [DecidableEq α] (a : α) :
        theorem Multiset.sum_hom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset α) {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) :
        theorem Multiset.prod_hom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset α) {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) :
        theorem Multiset.sum_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (g : ια) :
        Multiset.sum (Multiset.map (fun (i : ι) => f (g i)) s) = f (Multiset.sum (Multiset.map g s))
        theorem Multiset.prod_hom' {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) (g : ια) :
        Multiset.prod (Multiset.map (fun (i : ι) => f (g i)) s) = f (Multiset.prod (Multiset.map g s))
        theorem Multiset.sum_hom₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] (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.sum (Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s) = f (Multiset.sum (Multiset.map f₁ s)) (Multiset.sum (Multiset.map f₂ s))
        theorem Multiset.prod_hom₂ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [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₂ : ιβ) :
        Multiset.prod (Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s) = f (Multiset.prod (Multiset.map f₁ s)) (Multiset.prod (Multiset.map f₂ s))
        theorem Multiset.sum_hom_rel {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset ι) {r : αβProp} {f : ια} {g : ιβ} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b cr (f a + b) (g a + c)) :
        theorem Multiset.prod_hom_rel {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (s : Multiset ι) {r : αβProp} {f : ια} {g : ιβ} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b cr (f a * b) (g a * c)) :
        theorem Multiset.sum_map_zero {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} :
        Multiset.sum (Multiset.map (fun (x : ι) => 0) m) = 0
        theorem Multiset.prod_map_one {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} :
        Multiset.prod (Multiset.map (fun (x : ι) => 1) m) = 1
        @[simp]
        theorem Multiset.sum_map_add {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ια} {g : ια} :
        Multiset.sum (Multiset.map (fun (i : ι) => f i + g i) m) = Multiset.sum (Multiset.map f m) + Multiset.sum (Multiset.map g m)
        @[simp]
        theorem Multiset.prod_map_mul {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ια} {g : ια} :
        @[simp]
        theorem Multiset.prod_map_neg {α : Type u_2} [CommMonoid α] [HasDistribNeg α] (s : Multiset α) :
        Multiset.prod (Multiset.map Neg.neg s) = (-1) ^ Multiset.card s * Multiset.prod s
        theorem Multiset.sum_map_nsmul {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] {m : Multiset ι} {f : ια} {n : } :
        Multiset.sum (Multiset.map (fun (i : ι) => n f i) m) = n Multiset.sum (Multiset.map f m)
        theorem Multiset.prod_map_pow {ι : Type u_1} {α : Type u_2} [CommMonoid α] {m : Multiset ι} {f : ια} {n : } :
        Multiset.prod (Multiset.map (fun (i : ι) => f i ^ n) m) = Multiset.prod (Multiset.map f m) ^ n
        theorem Multiset.sum_map_sum_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] (m : Multiset β) (n : Multiset γ) {f : βγα} :
        Multiset.sum (Multiset.map (fun (a : β) => Multiset.sum (Multiset.map (fun (b : γ) => f a b) n)) m) = Multiset.sum (Multiset.map (fun (b : γ) => Multiset.sum (Multiset.map (fun (a : β) => f a b) m)) n)
        theorem Multiset.prod_map_prod_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] (m : Multiset β) (n : Multiset γ) {f : βγα} :
        Multiset.prod (Multiset.map (fun (a : β) => Multiset.prod (Multiset.map (fun (b : γ) => f a b) n)) m) = Multiset.prod (Multiset.map (fun (b : γ) => Multiset.prod (Multiset.map (fun (a : β) => f a b) m)) n)
        theorem Multiset.sum_induction {α : Type u_2} [AddCommMonoid α] (p : αProp) (s : Multiset α) (p_mul : ∀ (a b : α), p ap bp (a + b)) (p_one : p 0) (p_s : as, p a) :
        theorem Multiset.prod_induction {α : Type u_2} [CommMonoid α] (p : αProp) (s : Multiset α) (p_mul : ∀ (a b : α), p ap bp (a * b)) (p_one : p 1) (p_s : as, p a) :
        theorem Multiset.sum_induction_nonempty {α : Type u_2} [AddCommMonoid α] {s : Multiset α} (p : αProp) (p_mul : ∀ (a b : α), p ap bp (a + b)) (hs : s ) (p_s : as, p a) :
        theorem Multiset.prod_induction_nonempty {α : Type u_2} [CommMonoid α] {s : Multiset α} (p : αProp) (p_mul : ∀ (a b : α), p ap bp (a * b)) (hs : s ) (p_s : as, p a) :
        theorem Multiset.prod_dvd_prod_of_le {α : Type u_2} [CommMonoid α] {s : Multiset α} {t : Multiset α} (h : s t) :
        theorem Multiset.prod_dvd_prod_of_dvd {α : Type u_2} {β : Type u_3} [CommMonoid β] {S : Multiset α} (g1 : αβ) (g2 : αβ) (h : aS, g1 a g2 a) :

        Multiset.sum, the sum of the elements of a multiset, promoted to a morphism of AddCommMonoids.

        Equations
        • Multiset.sumAddMonoidHom = { toZeroHom := { toFun := Multiset.sum, map_zero' := }, map_add' := }
        Instances For
          @[simp]
          theorem Multiset.coe_sumAddMonoidHom {α : Type u_2} [AddCommMonoid α] :
          Multiset.sumAddMonoidHom = Multiset.sum
          theorem Multiset.prod_eq_zero {α : Type u_2} [CommMonoidWithZero α] {s : Multiset α} (h : 0 s) :
          theorem Multiset.prod_ne_zero {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} (h : 0s) :
          @[simp]
          theorem Multiset.sum_map_neg {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ια} :
          Multiset.sum (Multiset.map (fun (i : ι) => -f i) m) = -Multiset.sum (Multiset.map f m)
          @[simp]
          theorem Multiset.prod_map_inv {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ια} :
          @[simp]
          theorem Multiset.sum_map_sub {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ια} {g : ια} :
          Multiset.sum (Multiset.map (fun (i : ι) => f i - g i) m) = Multiset.sum (Multiset.map f m) - Multiset.sum (Multiset.map g m)
          @[simp]
          theorem Multiset.prod_map_div {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ια} {g : ια} :
          theorem Multiset.sum_map_zsmul {ι : Type u_1} {α : Type u_2} [SubtractionCommMonoid α] {m : Multiset ι} {f : ια} {n : } :
          Multiset.sum (Multiset.map (fun (i : ι) => n f i) m) = n Multiset.sum (Multiset.map f m)
          theorem Multiset.prod_map_zpow {ι : Type u_1} {α : Type u_2} [DivisionCommMonoid α] {m : Multiset ι} {f : ια} {n : } :
          Multiset.prod (Multiset.map (fun (i : ι) => f i ^ n) m) = Multiset.prod (Multiset.map f m) ^ n
          theorem Multiset.sum_map_mul_left {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ια} :
          Multiset.sum (Multiset.map (fun (i : ι) => a * f i) s) = a * Multiset.sum (Multiset.map f s)
          theorem Multiset.sum_map_mul_right {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ια} :
          Multiset.sum (Multiset.map (fun (i : ι) => f i * a) s) = Multiset.sum (Multiset.map f s) * a
          theorem Multiset.dvd_sum {α : Type u_2} [NonUnitalSemiring α] {a : α} {s : Multiset α} :
          (xs, a x)a Multiset.sum s

          Order #

          theorem Multiset.sum_nonneg {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} :
          (xs, 0 x)0 Multiset.sum s
          theorem Multiset.one_le_prod_of_one_le {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
          (xs, 1 x)1 Multiset.prod s
          theorem Multiset.single_le_sum {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} :
          (xs, 0 x)xs, x Multiset.sum s
          theorem Multiset.single_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
          (xs, 1 x)xs, x Multiset.prod s
          theorem Multiset.sum_le_card_nsmul {α : Type u_2} [OrderedAddCommMonoid α] (s : Multiset α) (n : α) (h : xs, x n) :
          Multiset.sum s Multiset.card s n
          theorem Multiset.prod_le_pow_card {α : Type u_2} [OrderedCommMonoid α] (s : Multiset α) (n : α) (h : xs, x n) :
          Multiset.prod s n ^ Multiset.card s
          theorem Multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} :
          (xs, 0 x)Multiset.sum s = 0xs, x = 0
          theorem Multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
          (xs, 1 x)Multiset.prod s = 1xs, x = 1
          theorem Multiset.sum_le_sum_of_rel_le {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} {t : Multiset α} (h : Multiset.Rel (fun (x x_1 : α) => x x_1) s t) :
          theorem Multiset.prod_le_prod_of_rel_le {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} {t : Multiset α} (h : Multiset.Rel (fun (x x_1 : α) => x x_1) s t) :
          theorem Multiset.sum_map_le_sum_map {ι : Type u_1} {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset ι} (f : ια) (g : ια) (h : is, f i g i) :
          theorem Multiset.prod_map_le_prod_map {ι : Type u_1} {α : Type u_2} [OrderedCommMonoid α] {s : Multiset ι} (f : ια) (g : ια) (h : is, f i g i) :
          theorem Multiset.sum_map_le_sum {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} (f : αα) (h : xs, f x x) :
          theorem Multiset.prod_map_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} (f : αα) (h : xs, f x x) :
          theorem Multiset.sum_le_sum_map {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} (f : αα) (h : xs, x f x) :
          theorem Multiset.prod_le_prod_map {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} (f : αα) (h : xs, x f x) :
          theorem Multiset.card_nsmul_le_sum {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} {a : α} (h : xs, a x) :
          Multiset.card s a Multiset.sum s
          theorem Multiset.pow_card_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} {a : α} (h : xs, a x) :
          a ^ Multiset.card s Multiset.prod s
          theorem Multiset.sum_lt_sum {ι : Type u_1} {α : Type u_2} [OrderedCancelAddCommMonoid α] {s : Multiset ι} {f : ια} {g : ια} (hle : is, f i g i) (hlt : ∃ i ∈ s, f i < g i) :
          theorem Multiset.prod_lt_prod' {ι : Type u_1} {α : Type u_2} [OrderedCancelCommMonoid α] {s : Multiset ι} {f : ια} {g : ια} (hle : is, f i g i) (hlt : ∃ i ∈ s, f i < g i) :
          theorem Multiset.sum_lt_sum_of_nonempty {ι : Type u_1} {α : Type u_2} [OrderedCancelAddCommMonoid α] {s : Multiset ι} {f : ια} {g : ια} (hs : s ) (hfg : is, f i < g i) :
          theorem Multiset.prod_lt_prod_of_nonempty' {ι : Type u_1} {α : Type u_2} [OrderedCancelCommMonoid α] {s : Multiset ι} {f : ια} {g : ια} (hs : s ) (hfg : is, f i < g i) :
          theorem Multiset.prod_nonneg {α : Type u_2} [OrderedCommSemiring α] {m : Multiset α} (h : am, 0 a) :
          theorem Multiset.sum_eq_zero {α : Type u_2} [AddCommMonoid α] {m : Multiset α} (h : xm, x = 0) :

          Slightly more general version of Multiset.sum_eq_zero_iff for a non-ordered AddMonoid

          theorem Multiset.prod_eq_one {α : Type u_2} [CommMonoid α] {m : Multiset α} (h : xm, x = 1) :

          Slightly more general version of Multiset.prod_eq_one_iff for a non-ordered Monoid

          theorem Multiset.le_sum_of_mem {α : Type u_2} [CanonicallyOrderedAddCommMonoid α] {m : Multiset α} {a : α} (h : a m) :
          theorem Multiset.le_prod_of_mem {α : Type u_2} [CanonicallyOrderedCommMonoid α] {m : Multiset α} {a : α} (h : a m) :
          theorem Multiset.le_sum_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : αβ) (p : αProp) (h_one : f 0 = 0) (hp_one : p 0) (h_mul : ∀ (a b : α), p ap bf (a + b) f a + f b) (hp_mul : ∀ (a b : α), p ap bp (a + b)) (s : Multiset α) (hps : as, p a) :
          theorem Multiset.le_prod_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [CommMonoid α] [OrderedCommMonoid β] (f : αβ) (p : αProp) (h_one : f 1 = 1) (hp_one : p 1) (h_mul : ∀ (a b : α), p ap bf (a * b) f a * f b) (hp_mul : ∀ (a b : α), p ap bp (a * b)) (s : Multiset α) (hps : as, p a) :
          theorem Multiset.le_sum_of_subadditive {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : αβ) (h_one : f 0 = 0) (h_mul : ∀ (a b : α), f (a + b) f a + f b) (s : Multiset α) :
          theorem Multiset.le_prod_of_submultiplicative {α : Type u_2} {β : Type u_3} [CommMonoid α] [OrderedCommMonoid β] (f : αβ) (h_one : f 1 = 1) (h_mul : ∀ (a b : α), f (a * b) f a * f b) (s : Multiset α) :
          theorem Multiset.le_sum_nonempty_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : αβ) (p : αProp) (h_mul : ∀ (a b : α), p ap bf (a + b) f a + f b) (hp_mul : ∀ (a b : α), p ap bp (a + b)) (s : Multiset α) (hs_nonempty : s ) (hs : as, p a) :
          theorem Multiset.le_prod_nonempty_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [CommMonoid α] [OrderedCommMonoid β] (f : αβ) (p : αProp) (h_mul : ∀ (a b : α), p ap bf (a * b) f a * f b) (hp_mul : ∀ (a b : α), p ap bp (a * b)) (s : Multiset α) (hs_nonempty : s ) (hs : as, p a) :
          theorem Multiset.le_sum_nonempty_of_subadditive {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : αβ) (h_mul : ∀ (a b : α), f (a + b) f a + f b) (s : Multiset α) (hs_nonempty : s ) :
          theorem Multiset.le_prod_nonempty_of_submultiplicative {α : Type u_2} {β : Type u_3} [CommMonoid α] [OrderedCommMonoid β] (f : αβ) (h_mul : ∀ (a b : α), f (a * b) f a * f b) (s : Multiset α) (hs_nonempty : s ) :
          @[simp]
          theorem Multiset.sum_map_singleton {α : Type u_2} (s : Multiset α) :
          Multiset.sum (Multiset.map (fun (a : α) => {a}) s) = s
          theorem Multiset.sum_nat_mod (s : Multiset ) (n : ) :
          Multiset.sum s % n = Multiset.sum (Multiset.map (fun (x : ) => x % n) s) % n
          theorem Multiset.prod_nat_mod (s : Multiset ) (n : ) :
          Multiset.prod s % n = Multiset.prod (Multiset.map (fun (x : ) => x % n) s) % n
          theorem Multiset.sum_int_mod (s : Multiset ) (n : ) :
          Multiset.sum s % n = Multiset.sum (Multiset.map (fun (x : ) => x % n) s) % n
          theorem Multiset.prod_int_mod (s : Multiset ) (n : ) :
          Multiset.prod s % n = Multiset.prod (Multiset.map (fun (x : ) => x % n) s) % n
          theorem map_multiset_sum {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {F : Type u_5} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Multiset α) :
          theorem map_multiset_prod {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {F : Type u_5} [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) :
          theorem AddMonoidHom.map_multiset_sum {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (f : α →+ β) (s : Multiset α) :
          theorem MonoidHom.map_multiset_prod {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (f : α →* β) (s : Multiset α) :