# Lemmas about `Multiset.sum` and `Multiset.prod` requiring extra algebra imports #

source
@[simp]
theorem Multiset.prod_map_neg {M : Type u_2} [CommMonoid M] [HasDistribNeg M] (s : Multiset M) :
(map Neg.neg s).prod = (-1) ^ s.card * s.prod
source
theorem Multiset.prod_eq_zero {M₀ : Type u_3} [CommMonoidWithZero M₀] {s : Multiset M₀} (h : 0 ∈ s) :
s.prod = 0
source
@[simp]
theorem Multiset.prod_eq_zero_iff {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀} :
s.prod = 0 ↔ 0 ∈ s
source
theorem Multiset.prod_ne_zero {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀} (h : 0 ∉ s) :
s.prod ≠ 0
source
theorem Multiset.sum_map_mul_left {ι : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] {a : R} {s : Multiset ι} {f : ι → R} :
(map (fun (i : ι) => a * f i) s).sum = a * (map f s).sum
source
theorem Multiset.sum_map_mul_right {ι : Type u_1} {R : Type u_4} [NonUnitalNonAssocSemiring R] {a : R} {s : Multiset ι} {f : ι → R} :
(map (fun (i : ι) => f i * a) s).sum = (map f s).sum * a
source
theorem Multiset.dvd_sum {R : Type u_4} [NonUnitalSemiring R] {s : Multiset R} {a : R} :
(∀ x ∈ s, a ∣ x) → a ∣ s.sum
source
theorem Multiset.prod_map_sum {R : Type u_4} [CommSemiring R] {s : Multiset (Multiset R)} :
(map sum s).prod = (map prod s.Sections).sum
source
theorem Multiset.prod_map_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {s : Multiset ι} {f g : ι → R} :
(map (fun (i : ι) => f i + g i) s).prod = (map (fun (p : Multiset ι × Multiset ι) => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
source
theorem Commute.multiset_sum_right {R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (a : R) (h : ∀ b ∈ s, Commute a b) :
Commute a s.sum
source
theorem Commute.multiset_sum_left {R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (b : R) (h : ∀ a ∈ s, Commute a b) :
Commute s.sum b