polynomial.eval_prod for multiset

Stream: Is there code for X?

[Riccardo Brasca]

I don't find the analogue of docs#polynomial.eval_prod for multiset. Is this my fault or it is really missing?

[Eric Wieser]

I'd say its not there, else the version you link to would be a one line proof as multiset.eval_prod _

[Riccardo Brasca]

Let's prove it :)

[Riccardo Brasca]

Well, it's not there but the statement is longer than the proof :grinning:

import data.polynomial.eval

universes u v

namespace polynomial

open multiset

lemma eval_prod_multiset {R : Type u} [comm_semiring R] {ι : Type v} (s : multiset ι)
  (p : ι → polynomial R) (x : R) : eval x (multiset.map p s).prod =
  (multiset.map (λ i, eval x (p i)) s).prod :=
multiset.induction_on s (by simp) (λ _ _ h, by simp [h])

end polynomial

[Yury G. Kudryashov]

Or you can use (polynomial.eval_ring_hom x).map_multiset_prod.

[Riccardo Brasca]

Nice!