English
The algebraic closure in E of the algebraic closure of F in E equals the bottom subfield in E.
Русский
Замыкание алгебраическое F внутри E, взятое повторно, равно нулю в E.
LaTeX
$$$ \\operatorname{algebraicClosure}(\\operatorname{algebraicClosure}_F E) E = \\perp $$$
Lean4
/-- 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 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⟩
