Commit 2025-08-28 17:04 ee7591b5

chore(Algebra): deduplicate Multiset.mem_sum and relax types (#28860) The existing two theorems are mostly duplicate to each other (the Finset one is more general)

theorem Finset.mem_sum {ι : Type u_1} {M : Type u_4} {f : ι → Multiset M} (s : Finset ι) (b : M) :
b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a
@[simp]
theorem Multiset.mem_sum {ι : Type u_1} {a : ι} {s : Finset ι} {m : ι → Multiset ι} :
a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

This is a property of Multiset so it should be in their name spaces. I fixed the typing on the Multiset version and deprecated the Finset one.