isAlgClosure — Mathlib

English

If E is algebraically closed, then the algebraic closure of F in E is an algebraic closure of F.

Русский

Если E алгебраически замкнуто, то algebraicClosure F E является алгебраическим замыканием F.

LaTeX

$$$ \\text{IsAlgClosure}_F(\\operatorname{algebraicClosure}_F E) $$$

Lean4

/-- 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⟩

Похожие утверждения