adjoin_rank_le_of_isAlgebraic_right

English

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

Русский

Если L — целевое промежуточное поле над F, алгебраично относительно F, то ранги удовлетворяют ≤.

LaTeX

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

Lean4

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

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