isIntegralClosure — Mathlib

English

The algebraic closure of F in E is the integral closure of F in E.

Русский

Алгебраическое замыкание F в E является интегральным замыканием F в E.

LaTeX

$$$ \\operatorname{algebraicClosure}_F(E) \\text{ is integrally closed over }F$$$

Lean4

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

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