feat(field_theory/algebraic_closure): define `is_alg_closed.splits_co…

…domain` (#7187)

Let `p : polynomial K` and `k` be an algebraically closed extension of `K`. Showing that `p` splits in `k` used to be a bit awkward because `is_alg_closed.splits` only gives `splits (p.map (f : k →+* K)) id`, which you still have to `simp` to `splits p f`.

This PR defines `is_alg_closed.splits_codomain`, showing `splits p f` directly by doing the `simp`ing for you. It also renames `polynomial.splits'` to `is_alg_closed.splits_domain`, for symmetry.

Zulip discussion starts [here](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Complex.20numbers.20sums/near/234481576)

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) :