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

@[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

theorem Multiset.prod_eq_zero {M₀ : Type u_3} [CommMonoidWithZero M₀] {s : Multiset M₀} (h : 0 ∈ s) : s.prod = 0

@[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

theorem Multiset.prod_ne_zero {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀} (h : ¬0 ∈ s) : s.prod ≠ 0

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

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

theorem Multiset.dvd_sum {R : Type u_4} [NonUnitalSemiring R] {s : Multiset R} {a : R} : (∀ (x : R), x ∈ s → a ∣ x) → a ∣ s.sum

theorem Multiset.prod_map_sum {R : Type u_4} [CommSemiring R] {s : Multiset (Multiset R)} : (map sum s).prod = (map prod s.Sections).sum

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

theorem Commute.multiset_sum_right {R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (a : R) (h : ∀ (b : R), b ∈ s → Commute a b) : Commute a s.sum

theorem Commute.multiset_sum_left {R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Multiset R) (b : R) (h : ∀ (a : R), a ∈ s → Commute a b) : Commute s.sum b