Commit 2020-10-14 08:24 20006f10

feat(data/polynomial/field_division, field_theory/splitting_field): Splits if enough roots (#4557) I have added some lemmas about polynomials that split. In particular the fact that if p has as many roots as its degree than it can be written as a product of (X - a) and so it splits. The proof of this for monic polynomial, in eq_prod_of_card_roots_monic, is rather messy and can probably be improved a lot.