no goals
R : Type u_1
S : Type ?u.2531
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum (Quotient.mk (List.isSetoid R) a)) = prod (map trop (Quotient.mk (List.isSetoid R) a))
simpa using List.trop_sum