[Merged by Bors] - feat(field_theory/splitting_field): Add image_root_set

[tb65536]

This PR adds a short lemma image_root_set and uses it to prove that is_splitting_field is preserved by algebra isomorphisms.

---

[alreadydone]

Can you add this lemma to this PR? Its proof needs this lemma. Should be right next to polynomial.is_splitting_field.alg_equiv, and we could even make an iff version.

lemma polynomial.is_splitting_field.of_alg_equiv (f : L ≃ₐ[K] L') (p : K[X])
  [is_splitting_field K L' p] : is_splitting_field K L p :=
begin
  have : splits (algebra_map K L) p,
  { rw ← f.symm.to_alg_hom.comp_algebra_map,
    exact splits_comp_of_splits _ _ (is_splitting_field.splits L' p) },
  refine ⟨this, subalgebra.map_injective f.to_alg_hom f.injective _⟩,
  rw [algebra.map_top, (algebra.range_top_iff_surjective f.to_alg_hom).2 f.surjective],
  erw [← algebra.adjoin_image, image_root_set this],
  exact is_splitting_field.adjoin_roots L' p,
end

[tb65536]

@alreadydone I've added that lemma, although I also extracted a useful sublemma that also came up in #15795

[riccardobrasca]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests