adjoin_rank_le_of_isAlgebraic_left

English

If L is intermediate field of F–K with IsAlgebraic F (L), then rank_E(adjoin_E(L)) ≤ rank_F L.

Русский

Если L алгебраичен над F, то ранг сверху не превышает ранг основания: ранк E(adjoin_E(L)) ≤ ранг F L.

LaTeX

$$$\operatorname{rank}_E(\mathrm{adjoin}_E(L)) \le \operatorname{rank}_F(L)$$$

Lean4

theorem adjoin_rank_le_of_isAlgebraic_left (L : IntermediateField F K) [halg : Algebra.IsAlgebraic F E] :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
  adjoin_rank_le_of_isAlgebraic E L (Or.inl halg)

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