mem_algebraicClosure — Mathlib

English

An element x ∈ S lies in the algebraic closure of R in S if and only if x is algebraic over R.

Русский

Элемент x ∈ S принадлежит алгебраическому замыканию над R в S тогда и только тогда, когда x алгебраичен над R.

LaTeX

$$$x \\in \\text{algebraicClosure}_R S \\iff \\IsAlgebraic_R x$$$

Lean4

theorem mem_algebraicClosure [IsDomain R] {x : S} : x ∈ algebraicClosure R S ↔ IsAlgebraic R x :=
  Iff.rfl

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