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

@[simp]

theorem Multiset.prod_map_neg {α : Type u_2} [CommMonoid α] [HasDistribNeg α] (s : Multiset α) : (Multiset.map Neg.neg s).prod = (-1) ^ Multiset.card s * s.prod

theorem Multiset.prod_eq_zero {α : Type u_2} [CommMonoidWithZero α] {s : Multiset α} (h : 0 ∈ s) : s.prod = 0

@[simp]

theorem Multiset.prod_eq_zero_iff {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} : s.prod = 0 ↔ 0 ∈ s

theorem Multiset.prod_ne_zero {α : Type u_2} [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {s : Multiset α} (h : 0 ∉ s) : s.prod ≠ 0

theorem Multiset.sum_map_mul_left {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ι → α} : (Multiset.map (fun (i : ι) => a * f i) s).sum = a * (Multiset.map f s).sum

theorem Multiset.sum_map_mul_right {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {a : α} {s : Multiset ι} {f : ι → α} : (Multiset.map (fun (i : ι) => f i * a) s).sum = (Multiset.map f s).sum * a

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

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

theorem Multiset.prod_map_add {ι : Type u_1} {α : Type u_2} [CommSemiring α] {s : Multiset ι} {f : ι → α} {g : ι → α} : (Multiset.map (fun (i : ι) => f i + g i) s).prod = (Multiset.map (fun (p : Multiset ι × Multiset ι) => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod) s.antidiagonal).sum

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

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