isAlgebraic_adjoin_iff — Mathlib

English

For domain R, and any set s ⊆ S, the algebraicity of the adjoin of s over R is equivalent to the algebraicity of every element of s over R.

Русский

Для домена R и множества s ⊆ S алгебраичность adjoin_R s эквивалентна алгебраичности каждого элемента x ∈ s над R.

LaTeX

$$$\\text{IsAlgebraic}_R\\big(\\operatorname{adjoin}_R s\\big) \\iff \\forall x \\in s, \\text{IsAlgebraic}_R x$$$

Lean4

theorem isAlgebraic_adjoin_iff [IsDomain R] {s : Set S} : (adjoin R s).IsAlgebraic ↔ ∀ x ∈ s, IsAlgebraic R x :=
  Algebra.adjoin_le_iff (S := Subalgebra.algebraicClosure R S)

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