algebraicClosure_eq_bot — Mathlib

English

The membership test for an element x in algebraicClosure F E coincides with x being algebraic over F.

Русский

Членство элемента x в algebraicClosure F E совпадает с тем, что x алгебраичен над F.

LaTeX

$$$ x \\in \\operatorname{algebraicClosure}_F(E) \\iff \\operatorname{IsAlgebraic}_F(x) $$$

Lean4

/-- The algebraic closure in `E` of the algebraic closure of `F` in `E` is equal to itself. -/
theorem algebraicClosure_eq_bot : algebraicClosure (algebraicClosure F E) E = ⊥ :=
  bot_unique fun x hx ↦ mem_bot.2 ⟨⟨x, isIntegral_trans x (mem_algebraicClosure_iff'.1 hx)⟩, rfl⟩

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