algebraicClosure_eq_integralClosure

English

If K is a field and S is a K-algebra, then the algebraicClosure K S equals the integralClosure K S.

Русский

Если K — поле и S — K-алгебра, то algebraicClosure K S совпадает с integralClosure K S.

LaTeX

$$$\\text{algebraicClosure}_K S = \\text{integralClosure}_K S$$$

Lean4

theorem algebraicClosure_eq_integralClosure {K} [Field K] [Algebra K S] : algebraicClosure K S = integralClosure K S :=
  SetLike.ext fun _ ↦ isAlgebraic_iff_isIntegral

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