eq_top_iff — Mathlib

English

The algebraic closure of F in E equals top if and only if E/F is algebraic.

Русский

Замыкание алгебраическое F в E равно верхнему пределу тогда и только тогда, когда E/ F является алгебраическим.

LaTeX

$$$ \\operatorname{algebraicClosure}_F(E) = \\top \\iff \\operatorname{IsAlgebraic}_F(E) $$$

Lean4

/-- The algebraic closure of `F` in `E` is equal to `E` if and only if `E / F` is
algebraic. -/
theorem eq_top_iff : algebraicClosure F E = ⊤ ↔ Algebra.IsAlgebraic F E :=
  ⟨fun h ↦ ⟨fun _ ↦ mem_algebraicClosure_iff.1 (h ▸ mem_top)⟩, fun _ ↦
    top_unique fun x _ ↦ mem_algebraicClosure_iff.2 (Algebra.IsAlgebraic.isAlgebraic x)⟩

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