mathlib3

6a5a6494 - chore(field_theory): move `polynomial.splits` to a new file (#17354)

chore(field_theory): move `polynomial.splits` to a new file (#17354) I noticed a lot of files use `polynomial.splits` without needing `splitting_field`. Since the definition of `splits` has a lot less dependencies than `splitting_field`, splitting the splitting field file hopefully helps recompilation a bit. The new files are: * `data.polynomial.splits`: definition of `polynomial.splits` and all lemmas not mentioning (`is_`)`splitting_field` * `ring_theory.adjoin.field`: some auxiliary lemmas on adjoining elements to a ring that are also used outside of `field_theory.splitting_field` Co-authored-by: Vierkantor <vierkantor@vierkantor.com>