subsingleton_of_finrank_adjoin_le_one

English

If for all x ∈ E we have finrank F F⟮x⟯ ≤ 1, then IntermediateField F E is a subsingleton.

Русский

Если для каждого x ∈ E finrank F F⟮x⟯ ≤ 1, то промежуточное поле F E — подсинглтон.

LaTeX

$$[FiniteDimensional F E] (∀ x : E, \operatorname{finrank} F F⟮x⟯ ≤ 1) → Subsingleton (IntermediateField F E)$$

Lean4

theorem subsingleton_of_finrank_adjoin_le_one [FiniteDimensional F E] (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) :
    Subsingleton (IntermediateField F E) :=
  subsingleton_of_bot_eq_top (bot_eq_top_of_finrank_adjoin_le_one h)

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