Root-set lemmas

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem Polynomial.prod_rootSet_eq_prod_aroots {K : Type u_1} {E : Type u_2} {M : Type u_3} [Field K] [Field E] [Algebra K E] [CommMonoid M] {p : Polynomial K} (hnodup : (p.aroots E).Nodup) (f : E → M) : ∏ β : ↑(p.rootSet E), f ↑β = (Multiset.map f (p.aroots E)).prod

For a polynomial without repeated roots in E, a product over the (coerced) rootSet equals the corresponding multiset product over aroots.