isAlgebraic_of_finite_intermediateField

English

If there are only finitely many intermediate fields between F and E, then every element of E is algebraic over F; i.e., Algebra.IsAlgebraic F E.

Русский

Если между F и E существует лишь конечное число промежуточных полей, то каждый элемент E является алгебраически над F.

LaTeX

$$$\text{Finite }(\text{IntermediateField } F E) \Rightarrow \text{Algebra.IsAlgebraic } F E$$$

Lean4

theorem isAlgebraic_of_finite_intermediateField [Finite (IntermediateField F E)] : Algebra.IsAlgebraic F E :=
  ⟨fun α ↦
    have ⟨_m, _n, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite fun n ↦ F⟮α ^ n⟯
    isAlgebraic_of_adjoin_eq_adjoin F E hneq heq⟩

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