mathlib3

a0ae2165 - feat(field_theory/splitting_field): generalize `splits` for `comm_ring K` (#16405)

feat(field_theory/splitting_field): generalize `splits` for `comm_ring K` (#16405) The definition of `splits` has been slightly changed for this change. Hence 2 lemmas `splits_iff` and `splits.def` are added for the `field K` case. I guess it may be helpful if we are able to talk about something like `splits i (p : ℤ[X])`?