diff --git a/src/field_theory/algebraic_closure.lean b/src/field_theory/algebraic_closure.lean
index aa45f64977879..86be958eeab46 100644
--- a/src/field_theory/algebraic_closure.lean
+++ b/src/field_theory/algebraic_closure.lean
@@ -44,12 +44,28 @@ open polynomial
 
 variables (k : Type u) [field k]
 
-/-- Typeclass for algebraically closed fields. -/
+/-- Typeclass for algebraically closed fields.
+
+To show `polynomial.splits p f` for an arbitrary ring homomorphism `f`,
+see `is_alg_closed.splits_codomain` and `is_alg_closed.splits_domain`.
+-/
 class is_alg_closed : Prop :=
 (splits : ∀ p : polynomial k, p.splits $ ring_hom.id k)
 
-theorem polynomial.splits' {k K : Type*} [field k] [is_alg_closed k] [field K] {f : k →+* K}
-  (p : polynomial k) : p.splits f :=
+/-- Every polynomial splits in the field extension `f : K →+* k` if `k` is algebraically closed.
+
+See also `is_alg_closed.splits_domain` for the case where `K` is algebraically closed.
+-/
+theorem is_alg_closed.splits_codomain {k K : Type*} [field k] [is_alg_closed k] [field K]
+  {f : K →+* k} (p : polynomial K) : p.splits f :=
+by { convert is_alg_closed.splits (p.map f), simp [splits_map_iff] }
+
+/-- Every polynomial splits in the field extension `f : K →+* k` if `K` is algebraically closed.
+
+See also `is_alg_closed.splits_codomain` for the case where `k` is algebraically closed.
+-/
+theorem is_alg_closed.splits_domain {k K : Type*} [field k] [is_alg_closed k] [field K]
+  {f : k →+* K} (p : polynomial k) : p.splits f :=
 polynomial.splits_of_splits_id _ $ is_alg_closed.splits _
 
 namespace is_alg_closed
@@ -66,7 +82,7 @@ theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p →
 lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz : p ≠ 0)
   (hp : irreducible p) :
   p.degree = 1 :=
-degree_eq_one_of_irreducible_of_splits h_nz hp (polynomial.splits' _)
+degree_eq_one_of_irreducible_of_splits h_nz hp (is_alg_closed.splits_codomain _)
 
 lemma algebra_map_surjective_of_is_integral {k K : Type*} [field k] [domain K]
   [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_integral k K) :