mathlib3

0a34b827 - feat(field_theory/splitting_field): Add `image_root_set` (#15743)

feat(field_theory/splitting_field): Add `image_root_set` (#15743) This PR adds a short lemma `image_root_set` and uses it to prove that `is_splitting_field` is preserved by algebra isomorphisms. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>