mathlib3

9f55ed70 - feat(data/polynomial/ring_division): make `polynomial.roots` a multiset (#4061)

feat(data/polynomial/ring_division): make `polynomial.roots` a multiset (#4061) The original definition of `polynomial.roots` was basically "while ∃ x, p.is_root x { finset.insert x polynomial.roots }", so it was not too hard to replace this with `multiset.cons`. I tried to refactor most usages of `polynomial.roots` to talk about the multiset instead of coercing it to a finset, since that should give a bit more power to the results.