Commit 2020-09-10 01:34 9f55ed70

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.