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

theorem Multiset.dvd_prod {α : Type u_1} [CommMonoid α] {s : Multiset α} {a : α} : a ∈ s → a ∣ Multiset.prod s

@[simp]

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

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

@[simp]

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

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

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

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

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