isAlgebraic_tower_bot — Mathlib

English

If the ambient extension L/K is algebraic, then every intermediate field S ⊆ L is algebraic over K; i.e., the tower from K to S to L preserves algebraicity downwards.

Русский

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

LaTeX

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

Lean4

instance isAlgebraic_tower_bot [Algebra.IsAlgebraic K L] : Algebra.IsAlgebraic K S :=
  Algebra.IsAlgebraic.of_injective S.val S.val.injective

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