isAlgebraic_adjoin_iff_isAlgebraic

English

F(S)/F is algebraic iff every element of S is algebraic over F.

Русский

F(S)/F алгебраично тогда и только тогда, когда каждый элемент S алгебраичен над F.

LaTeX

$$$ \\operatorname{IsAlgebraic}_F(\\operatorname{adjoin}_F S) \\iff \\forall x \\in S,\\ IsAlgebraic}_F(x) $$$

Lean4

/-- `F(S) / F` is a algebraic extension if and only if all elements of `S` are
algebraic elements. -/
theorem isAlgebraic_adjoin_iff_isAlgebraic {S : Set E} :
    Algebra.IsAlgebraic F (adjoin F S) ↔ ∀ x ∈ S, IsAlgebraic F x :=
  ((le_algebraicClosure_iff F E _).symm.trans
    (adjoin_le_iff.trans <| forall_congr' <| fun _ => Iff.imp Iff.rfl mem_algebraicClosure_iff))

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