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

theorem Multiset.sum_eq_zero_iff {α : Type u_1} [CanonicallyOrderedAddMonoid α] {m : Multiset α} : Multiset.sum m = 0 ↔ ∀ (x : α), x ∈ m → x = 0

theorem Multiset.prod_eq_one_iff {α : Type u_1} [CanonicallyOrderedMonoid α] {m : Multiset α} : Multiset.prod m = 1 ↔ ∀ (x : α), x ∈ m → x = 1

@[simp]

theorem CanonicallyOrderedCommSemiring.multiset_prod_pos {R : Type u_2} [CanonicallyOrderedCommSemiring R] [Nontrivial R] {m : Multiset R} : 0 < Multiset.prod m ↔ ∀ (x : R), x ∈ m → 0 < x

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

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