diff --git a/Mathlib.lean b/Mathlib.lean
index f99c43c96a2ad..fd19b34c2864f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2791,6 +2791,7 @@ import Mathlib.Dynamics.TopologicalEntropy.Semiconj
 import Mathlib.FieldTheory.AbelRuffini
 import Mathlib.FieldTheory.AbsoluteGaloisGroup
 import Mathlib.FieldTheory.Adjoin
+import Mathlib.FieldTheory.AlgebraicClosure
 import Mathlib.FieldTheory.AxGrothendieck
 import Mathlib.FieldTheory.Cardinality
 import Mathlib.FieldTheory.ChevalleyWarning
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
index 0be6a81f50b0a..bb02c5b46fae0 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
@@ -386,6 +386,10 @@ lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab :
   rw [cfc_le_iff id (fun _ => ‖b‖) a] at h₂
   exact h₂ ‖a‖ <| norm_mem_spectrum_of_nonneg ha
 
+theorem nnnorm_le_nnnorm_of_nonneg_of_le {a : A} {b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) :
+    ‖a‖₊ ≤ ‖b‖₊ :=
+  norm_le_norm_of_nonneg_of_le ha hab
+
 lemma conjugate_le_norm_smul {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) :
     star a * b * a ≤ ‖b‖ • (star a * a) := by
   suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by
@@ -421,3 +425,35 @@ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by
 end CStarAlgebra
 
 end CStar_nonunital
+
+section Pow
+
+namespace CStarAlgebra
+
+variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+
+lemma pow_nonneg {a : A} (ha : 0 ≤ a := by cfc_tac) (n : ℕ) : 0 ≤ a ^ n := by
+  rw [← cfc_pow_id (R := ℝ≥0) a]
+  exact cfc_nonneg_of_predicate
+
+lemma pow_monotone {a : A} (ha : 1 ≤ a) : Monotone (a ^ · : ℕ → A) := by
+  have ha' : 0 ≤ a := zero_le_one.trans ha
+  intro n m hnm
+  simp only
+  rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
+  rw [CFC.one_le_iff (R := ℝ) a] at ha
+  peel ha with x hx _
+  exact pow_le_pow_right₀ (ha x hx) hnm
+
+lemma pow_antitone {a : A} (ha₀ : 0 ≤ a := by cfc_tac) (ha₁ : a ≤ 1) :
+    Antitone (a ^ · : ℕ → A) := by
+  intro n m hnm
+  simp only
+  rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
+  rw [CFC.le_one_iff (R := ℝ) a] at ha₁
+  peel ha₁ with x hx _
+  exact pow_le_pow_of_le_one (spectrum_nonneg_of_nonneg ha₀ hx) (ha₁ x hx) hnm
+
+end CStarAlgebra
+
+end Pow
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
index 879cc599b5765..9e7b880fc4e4d 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
@@ -85,47 +85,16 @@ section Topology
 
 variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]
 
-theorem LinearMap.hasBasis_weakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
-    (𝓝 (0 : WeakBilin B)).HasBasis B.toSeminormFamily.basisSets _root_.id := by
-  let p := B.toSeminormFamily
-  rw [nhds_induced, nhds_pi]
-  simp only [map_zero, LinearMap.zero_apply]
-  have h := @Metric.nhds_basis_ball 𝕜 _ 0
-  have h' := Filter.hasBasis_pi fun _ : F => h
-  have h'' := Filter.HasBasis.comap (fun x y => B x y) h'
-  refine h''.to_hasBasis ?_ ?_
-  · rintro (U : Set F × (F → ℝ)) hU
-    cases' hU with hU₁ hU₂
-    simp only [_root_.id]
-    let U' := hU₁.toFinset
-    by_cases hU₃ : U.fst.Nonempty
-    · have hU₃' : U'.Nonempty := hU₁.toFinset_nonempty.mpr hU₃
-      refine ⟨(U'.sup p).ball 0 <| U'.inf' hU₃' U.snd, p.basisSets_mem _ <|
-        (Finset.lt_inf'_iff _).2 fun y hy => hU₂ y <| hU₁.mem_toFinset.mp hy, fun x hx y hy => ?_⟩
-      simp only [Set.mem_preimage, Set.mem_pi, mem_ball_zero_iff]
-      rw [Seminorm.mem_ball_zero] at hx
-      rw [← LinearMap.toSeminormFamily_apply]
-      have hyU' : y ∈ U' := (Set.Finite.mem_toFinset hU₁).mpr hy
-      have hp : p y ≤ U'.sup p := Finset.le_sup hyU'
-      refine lt_of_le_of_lt (hp x) (lt_of_lt_of_le hx ?_)
-      exact Finset.inf'_le _ hyU'
-    rw [Set.not_nonempty_iff_eq_empty.mp hU₃]
-    simp only [Set.empty_pi, Set.preimage_univ, Set.subset_univ, and_true]
-    exact Exists.intro ((p 0).ball 0 1) (p.basisSets_singleton_mem 0 one_pos)
-  rintro U (hU : U ∈ p.basisSets)
-  rw [SeminormFamily.basisSets_iff] at hU
-  rcases hU with ⟨s, r, hr, hU⟩
-  rw [hU]
-  refine ⟨(s, fun _ => r), ⟨by simp only [s.finite_toSet], fun y _ => hr⟩, fun x hx => ?_⟩
-  simp only [Set.mem_preimage, Set.mem_pi, Finset.mem_coe, mem_ball_zero_iff] at hx
-  simp only [_root_.id, Seminorm.mem_ball, sub_zero]
-  refine Seminorm.finset_sup_apply_lt hr fun y hy => ?_
-  rw [LinearMap.toSeminormFamily_apply]
-  exact hx y hy
-
 theorem LinearMap.weakBilin_withSeminorms (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
     WithSeminorms (LinearMap.toSeminormFamily B : F → Seminorm 𝕜 (WeakBilin B)) :=
-  SeminormFamily.withSeminorms_of_hasBasis _ B.hasBasis_weakBilin
+  let e : F ≃ (Σ _ : F, Fin 1) := .symm <| .sigmaUnique _ _
+  have : Nonempty (Σ _ : F, Fin 1) := e.symm.nonempty
+  withSeminorms_induced (withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜))
+    (LinearMap.ltoFun 𝕜 F 𝕜 ∘ₗ B : (WeakBilin B) →ₗ[𝕜] (F → 𝕜)) |>.congr_equiv e
+
+theorem LinearMap.hasBasis_weakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
+    (𝓝 (0 : WeakBilin B)).HasBasis B.toSeminormFamily.basisSets _root_.id :=
+  LinearMap.weakBilin_withSeminorms B |>.hasBasis
 
 end Topology
 
diff --git a/Mathlib/FieldTheory/AlgebraicClosure.lean b/Mathlib/FieldTheory/AlgebraicClosure.lean
new file mode 100644
index 0000000000000..d82e2ddcf8fd7
--- /dev/null
+++ b/Mathlib/FieldTheory/AlgebraicClosure.lean
@@ -0,0 +1,202 @@
+/-
+Copyright (c) 2024 Jiedong Jiang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu, Jiedong Jiang
+-/
+import Mathlib.FieldTheory.NormalClosure
+import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.FieldTheory.IntermediateField.Algebraic
+
+/-!
+# Relative Algebraic Closure
+
+In this file we construct the relative algebraic closure of a field extension.
+
+## Main Definitions
+
+- `algebraicClosure F E` is the relative algebraic closure (i.e. the maximal algebraic subextension)
+  of the field extension `E / F`, which is defined to be the integral closure of `F` in `E`.
+
+-/
+noncomputable section
+
+open Polynomial FiniteDimensional IntermediateField Field
+
+variable (F E : Type*) [Field F] [Field E] [Algebra F E]
+variable {K : Type*} [Field K] [Algebra F K]
+
+/--
+The *relative algebraic closure* of a field `F` in a field extension `E`,
+also called the *maximal algebraic subextension* of `E / F`,
+is defined to be the subalgebra `integralClosure F E`
+upgraded to an intermediate field (since `F` and `E` are both fields).
+This is exactly the intermediate field of `E / F` consisting of all integral/algebraic elements.
+-/
+def algebraicClosure : IntermediateField F E :=
+  Algebra.IsAlgebraic.toIntermediateField (integralClosure F E)
+
+variable {F E}
+
+/-- An element is contained in the algebraic closure of `F` in `E` if and only if
+it is an integral element. -/
+theorem mem_algebraicClosure_iff' {x : E} :
+    x ∈ algebraicClosure F E ↔ IsIntegral F x := Iff.rfl
+
+/-- An element is contained in the algebraic closure of `F` in `E` if and only if
+it is an algebraic element. -/
+theorem mem_algebraicClosure_iff {x : E} :
+    x ∈ algebraicClosure F E ↔ IsAlgebraic F x := isAlgebraic_iff_isIntegral.symm
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
+`algebraicClosure F K` if and only if `x` is contained in `algebraicClosure F E`. -/
+theorem map_mem_algebraicClosure_iff (i : E →ₐ[F] K) {x : E} :
+    i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E := by
+  simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]
+
+namespace algebraicClosure
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the preimage of
+`algebraicClosure F K` under the map `i` is equal to `algebraicClosure F E`. -/
+theorem comap_eq_of_algHom (i : E →ₐ[F] K) :
+    (algebraicClosure F K).comap i = algebraicClosure F E := by
+  ext x
+  exact map_mem_algebraicClosure_iff i
+
+/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then the image of `algebraicClosure F E`
+under the map `i` is contained in `algebraicClosure F K`. -/
+theorem map_le_of_algHom (i : E →ₐ[F] K) :
+    (algebraicClosure F E).map i ≤ algebraicClosure F K :=
+  map_le_iff_le_comap.2 (comap_eq_of_algHom i).ge
+
+variable (F) in
+/-- If `K / E / F` is a field extension tower, such that `K / E` has no non-trivial algebraic
+subextensions (this means that it is purely transcendental),
+then the image of `algebraicClosure F E` in `K` is equal to `algebraicClosure F K`. -/
+theorem map_eq_of_algebraicClosure_eq_bot [Algebra E K] [IsScalarTower F E K]
+    (h : algebraicClosure E K = ⊥) :
+    (algebraicClosure F E).map (IsScalarTower.toAlgHom F E K) = algebraicClosure F K := by
+  refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
+  obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
+    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)
+  exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩
+
+/-- If `i` is an `F`-algebra isomorphism of `E` and `K`, then the image of `algebraicClosure F E`
+under the map `i` is equal to `algebraicClosure F K`. -/
+theorem map_eq_of_algEquiv (i : E ≃ₐ[F] K) :
+    (algebraicClosure F E).map i = algebraicClosure F K :=
+  (map_le_of_algHom i.toAlgHom).antisymm
+    (fun x h ↦ ⟨_, (map_mem_algebraicClosure_iff i.symm).2 h, by simp⟩)
+
+/-- If `E` and `K` are isomorphic as `F`-algebras, then `algebraicClosure F E` and
+`algebraicClosure F K` are also isomorphic as `F`-algebras. -/
+def algEquivOfAlgEquiv (i : E ≃ₐ[F] K) :
+    algebraicClosure F E ≃ₐ[F] algebraicClosure F K :=
+  (intermediateFieldMap i _).trans (equivOfEq (map_eq_of_algEquiv i))
+
+alias AlgEquiv.algebraicClosure := algebraicClosure.algEquivOfAlgEquiv
+
+variable (F E K)
+
+/-- The algebraic closure of `F` in `E` is algebraic over `F`. -/
+instance isAlgebraic : Algebra.IsAlgebraic F (algebraicClosure F E) :=
+  ⟨fun x ↦
+    isAlgebraic_iff.mpr (IsAlgebraic.isIntegral (mem_algebraicClosure_iff.mp x.2)).isAlgebraic⟩
+
+/-- The algebraic closure of `F` in `E` is the integral closure of `F` in `E`. -/
+instance isIntegralClosure : IsIntegralClosure (algebraicClosure F E) F E :=
+  inferInstanceAs (IsIntegralClosure (integralClosure F E) F E)
+
+end algebraicClosure
+
+variable (F E K)
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if all of its elements are algebraic over `F`. -/
+theorem le_algebraicClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsAlgebraic F x) :
+    L ≤ algebraicClosure F E := fun x h ↦ by
+  simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
+    Algebra.id.map_eq_id, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if it is algebraic over `F`. -/
+theorem le_algebraicClosure (L : IntermediateField F E) [Algebra.IsAlgebraic F L] :
+    L ≤ algebraicClosure F E := le_algebraicClosure' F E (Algebra.IsAlgebraic.isAlgebraic)
+
+/-- An intermediate field of `E / F` is contained in the algebraic closure of `F` in `E`
+if and only if it is algebraic over `F`. -/
+theorem le_algebraicClosure_iff (L : IntermediateField F E) :
+    L ≤ algebraicClosure F E ↔ Algebra.IsAlgebraic F L :=
+  ⟨fun h ↦ ⟨fun x ↦ by simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
+    IntermediateField.algebraMap_apply,
+    Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2⟩,
+    fun _ ↦ le_algebraicClosure _ _ _⟩
+
+namespace algebraicClosure
+
+/-- The algebraic closure in `E` of the algebraic closure of `F` in `E` is equal to itself. -/
+theorem algebraicClosure_eq_bot :
+    algebraicClosure (algebraicClosure F E) E = ⊥ :=
+  bot_unique fun x hx ↦ mem_bot.2
+    ⟨⟨x, isIntegral_trans x (mem_algebraicClosure_iff'.1 hx)⟩, rfl⟩
+
+/-- The normal closure in `E/F` of the algebraic closure of `F` in `E` is equal to itself. -/
+theorem normalClosure_eq_self :
+    normalClosure F (algebraicClosure F E) E = algebraicClosure F E :=
+  le_antisymm (normalClosure_le_iff.2 fun i ↦
+    haveI : Algebra.IsAlgebraic F i.fieldRange := (AlgEquiv.ofInjectiveField i).isAlgebraic
+    le_algebraicClosure F E _) (le_normalClosure _)
+
+end algebraicClosure
+
+/-- If `E / F` is a field extension and `E` is algebraically closed, then the algebraic closure
+of `F` in `E` is equal to `F` if and only if `F` is algebraically closed. -/
+theorem IsAlgClosed.algebraicClosure_eq_bot_iff [IsAlgClosed E] :
+    algebraicClosure F E = ⊥ ↔ IsAlgClosed F := by
+  refine ⟨fun h ↦ IsAlgClosed.of_exists_root _ fun p hmon hirr ↦ ?_,
+    fun _ ↦ IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic _⟩
+  obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne'
+  obtain ⟨x, rfl⟩ := h ▸ mem_algebraicClosure_iff'.2 (minpoly.ne_zero_iff.1 <|
+    ne_zero_of_dvd_ne_zero hmon.ne_zero (minpoly.dvd _ x hx))
+  exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩
+
+/-- `F(S) / F` is a algebraic extension if and only if all elements of `S` are
+algebraic elements. -/
+theorem IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic {S : Set E} :
+    Algebra.IsAlgebraic F (adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x :=
+  ((le_algebraicClosure_iff F E _).symm.trans (adjoin_le_iff.trans <| forall_congr' <|
+    fun _ => Iff.imp Iff.rfl mem_algebraicClosure_iff))
+
+namespace algebraicClosure
+
+/-- If `E` is algebraically closed, then the algebraic closure of `F` in `E` is an absolute
+algebraic closure of `F`. -/
+instance isAlgClosure [IsAlgClosed E] : IsAlgClosure F (algebraicClosure F E) :=
+  ⟨(IsAlgClosed.algebraicClosure_eq_bot_iff _ E).mp (algebraicClosure_eq_bot F E),
+    isAlgebraic F E⟩
+
+/-- The algebraic closure of `F` in `E` is equal to `E` if and only if `E / F` is
+algebraic. -/
+theorem eq_top_iff : algebraicClosure F E = ⊤ ↔ Algebra.IsAlgebraic F E :=
+  ⟨fun h ↦ ⟨fun _ ↦ mem_algebraicClosure_iff.1 (h ▸ mem_top)⟩,
+    fun _ ↦ top_unique fun x _ ↦ mem_algebraicClosure_iff.2 (Algebra.IsAlgebraic.isAlgebraic x)⟩
+
+/-- If `K / E / F` is a field extension tower, then `algebraicClosure F K` is contained in
+`algebraicClosure E K`. -/
+theorem le_restrictScalars [Algebra E K] [IsScalarTower F E K] :
+    algebraicClosure F K ≤ (algebraicClosure E K).restrictScalars F :=
+  fun _ h ↦ mem_algebraicClosure_iff.2 <| IsAlgebraic.tower_top E (mem_algebraicClosure_iff.1 h)
+
+/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then
+`algebraicClosure F K` is equal to `algebraicClosure E K`. -/
+theorem eq_restrictScalars_of_isAlgebraic [Algebra E K] [IsScalarTower F E K]
+    [Algebra.IsAlgebraic F E] : algebraicClosure F K = (algebraicClosure E K).restrictScalars F :=
+  (algebraicClosure.le_restrictScalars F E K).antisymm fun _ h ↦
+    isIntegral_trans _ h
+
+/-- If `K / E / F` is a field extension tower, then `E` adjoin `algebraicClosure F K` is contained
+in `algebraicClosure E K`. -/
+theorem adjoin_le [Algebra E K] [IsScalarTower F E K] :
+    adjoin E (algebraicClosure F K) ≤ algebraicClosure E K :=
+  adjoin_le_iff.2 <| le_restrictScalars F E K
+
+end algebraicClosure
diff --git a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
index 326f408a7e4ff..fadc8889330f0 100644
--- a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
@@ -15,7 +15,7 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 open Module
 
-variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
   {S : IntermediateField K L}
 
 theorem IntermediateField.coe_isIntegral_iff {R : Type*} [CommRing R] [Algebra R K] [Algebra R L]
@@ -33,11 +33,6 @@ def Subalgebra.IsAlgebraic.toIntermediateField {S : Subalgebra K L} (hS : S.IsAl
 abbrev Algebra.IsAlgebraic.toIntermediateField (S : Subalgebra K L) [Algebra.IsAlgebraic K S] :
     IntermediateField K L := (S.isAlgebraic_iff.mpr ‹_›).toIntermediateField
 
-/-- The algebraic closure of a field `K` in an extension `L`, the subalgebra `integralClosure K L`
-upgraded to an intermediate field (when `K` and `L` are both fields). -/
-def algebraicClosure : IntermediateField K L :=
-  Algebra.IsAlgebraic.toIntermediateField (integralClosure K L)
-
 namespace IntermediateField
 
 instance isAlgebraic_tower_bot [Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic K S :=
diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean
index ee4583757d618..356b47cef750e 100644
--- a/Mathlib/FieldTheory/Minpoly/Basic.lean
+++ b/Mathlib/FieldTheory/Minpoly/Basic.lean
@@ -58,6 +58,9 @@ theorem ne_zero [Nontrivial A] (hx : IsIntegral A x) : minpoly A x ≠ 0 :=
 theorem eq_zero (hx : ¬IsIntegral A x) : minpoly A x = 0 :=
   dif_neg hx
 
+theorem ne_zero_iff [Nontrivial A] : minpoly A x ≠ 0 ↔ IsIntegral A x :=
+  ⟨fun h => of_not_not <| eq_zero.mt h, ne_zero⟩
+
 theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
     minpoly A (f x) = minpoly A x := by
   simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
diff --git a/Mathlib/RingTheory/Adjoin/Field.lean b/Mathlib/RingTheory/Adjoin/Field.lean
index a3b2407a38ac4..25bf90e6eb79c 100644
--- a/Mathlib/RingTheory/Adjoin/Field.lean
+++ b/Mathlib/RingTheory/Adjoin/Field.lean
@@ -116,6 +116,7 @@ end
 
 variable [Algebra K M] [IsScalarTower R K M] {x : M}
 
+/-- The `RingHom` version of `IsIntegral.minpoly_splits_tower_top`.  -/
 theorem IsIntegral.minpoly_splits_tower_top' (int : IsIntegral R x) {f : K →+* L}
     (h : Splits (f.comp <| algebraMap R K) (minpoly R x)) :
     Splits f (minpoly K x) :=
diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean
index 89dc73d0fbe22..1d1e4ac64d686 100644
--- a/Mathlib/RingTheory/Algebraic.lean
+++ b/Mathlib/RingTheory/Algebraic.lean
@@ -296,6 +296,12 @@ alias ⟨IsAlgebraic.isIntegral, _⟩ := isAlgebraic_iff_isIntegral
 protected instance Algebra.IsAlgebraic.isIntegral [Algebra.IsAlgebraic K A] :
     Algebra.IsIntegral K A := Algebra.isAlgebraic_iff_isIntegral.mp ‹_›
 
+variable (K) in
+theorem Algebra.IsAlgebraic.of_isIntegralClosure (B C : Type*)
+    [CommRing B] [CommRing C] [Algebra K B] [Algebra K C] [Algebra B C]
+    [IsScalarTower K B C] [IsIntegralClosure B K C] : Algebra.IsAlgebraic K B :=
+  Algebra.isAlgebraic_iff_isIntegral.mpr (IsIntegralClosure.isIntegral_algebra K C)
+
 end Field
 
 section