English
If x ∈ L is integral over K, then the natDegree of minpoly K x divides finrank K L.
Русский
Если x интеграл над K, то natDegree(minpoly K x) делит finrank_K L.
LaTeX
$$\( \operatorname{natDegree}(\minpoly K x) \mid \operatorname{finrank}_K L \)$$
Lean4
/-- A compositum of algebraic extensions is algebraic -/
theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L} (h : ∀ i, Algebra.IsAlgebraic K (t i)) :
Algebra.IsAlgebraic K (⨆ i, t i : IntermediateField K L) :=
by
constructor
rintro ⟨x, hx⟩
obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx
rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := (· ∈ _)) x hx, ← isAlgebraic_iff]
haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))
apply IsAlgebraic.of_finite
