algebraicClosure_toSubalgebra — Mathlib

English

The algebraic closure viewed as an intermediate field coincides with the integral closure viewed as a subalgebra.

Русский

Замыкание по алгебраическим элементам, как промежуточное поле, совпадает с интегральным замыканием как подалгеброй.

LaTeX

$$$$\text{algebraicClosure } F E := \text{toIntermediateField}(\text{integralClosure } F E)$$$$

Lean4

theorem algebraicClosure_toSubalgebra : (algebraicClosure F E).toSubalgebra = integralClosure F E :=
  rfl

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