∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (s : Multiset (Polynomial R)) (x : S), Polynomial.eval₂ f x s.prod = (Multiset.map (Polynomial.eval₂ f x) s).prod