mem_algebraicClosure_iff — Mathlib

English

An element lies in algebraicClosure F E if and only if it is algebraic over F.

Русский

Элемент принадлежит algebraicClosure F E тогда и только тогда, когда он алгебраический над F.

LaTeX

$$$$x \in \text{algebraicClosure } F E \iff \text{IsAlgebraic } F x$$$$

Lean4

/-- An element is contained in the algebraic closure of `F` in `E` if and only if
it is an algebraic element. -/
theorem mem_algebraicClosure_iff {x : E} : x ∈ algebraicClosure F E ↔ IsAlgebraic F x :=
  isAlgebraic_iff_isIntegral.symm

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