isAlgebraic_adjoin — Mathlib

English

A directed supremum (iSup) of algebraic extensions over K remains algebraic over K.

Русский

Объединение (supremum) направленного семейства алгебраических расширений над K остаётся алгебраическим над K.

LaTeX

$$If (t i) is a family of intermediate fields with each IsAlgebraic K (t i), then IsAlgebraic K (⨆ i, t i).$$

Lean4

theorem isAlgebraic_adjoin {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) : Algebra.IsAlgebraic K (adjoin K S) :=
  by
  rw [← biSup_adjoin_simple, ← iSup_subtype'']
  exact isAlgebraic_iSup fun x ↦ isAlgebraic_adjoin_simple (hS x x.2)

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