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 ∣ s.prod

@[simp]

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

theorem Multiset.fst_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.1 = (Multiset.map Prod.fst s).sum

theorem Multiset.fst_prod {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.1 = (Multiset.map Prod.fst s).prod

theorem Multiset.snd_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCommMonoid β] (s : Multiset (α × β)) : s.sum.2 = (Multiset.map Prod.snd s).sum

theorem Multiset.snd_prod {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoid β] (s : Multiset (α × β)) : s.prod.2 = (Multiset.map Prod.snd s).prod

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

@[simp]

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

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

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

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

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