isAlgebraic_tower_top — Mathlib

English

If L/K is algebraic, then L is algebraic over any intermediate field S ⊆ L; i.e., the top of the tower is algebraic over every intermediate field.

Русский

Если L/K алгебраическое, то L алгебраично относительно любого промежуточного поля S ⊆ L; то есть вершина башни алгебраична над любым S.

LaTeX

$$$ [Algebra.IsAlgebraic K L] \Rightarrow [Algebra.IsAlgebraic S L] $$$

Lean4

instance isAlgebraic_tower_top [Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic S L :=
  Algebra.IsAlgebraic.tower_top (K := K) S

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