feat(FieldTheory/AlgebraicClosure): A polynomial splits in E implies it splits in algebraicClosure F E (#18331)

Add a lemma saying a polynomial splits in `E` implies it splits in `algebraicClosure F E`.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Jiang Jiedong <107380768+jjdishere@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Author: 3 people

Mathlib/FieldTheory/AlgebraicClosure.lean

@@ -200,3 +200,12 @@ theorem adjoin_le [Algebra E K] [IsScalarTower F E K] :
   adjoin_le_iff.2 <| le_restrictScalars F E K
 
 end algebraicClosure
+
+variable {F}
+/--
+Let `E / F` be a field extension. If a polynomial `p`
+splits in `E`, then it splits in the relative algebraic closure of `F` in `E` already.
+-/
+theorem Splits.algebraicClosure {p : F[X]} (h : p.Splits (algebraMap F E)) :
+    p.Splits (algebraMap F (algebraicClosure F E)) :=
+  splits_of_splits h fun _ hx ↦ (isAlgebraic_of_mem_rootSet hx).isIntegral