mathlib

20006f10 - feat(data/polynomial/field_division, field_theory/splitting_field): Splits if enough roots (#4557)

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. Co-authored-by: Johan Commelin <johan@commelin.net>