finrank_eq_one_iff_eq_top — Mathlib

English

For an intermediate field K of E over F, finrank K E equals 1 if and only if K is the top field.

Русский

Для промежуточного поля K внутри E над F размерность E как векторного пространства над K равна 1 тогда и только тогда K совпадает с верхним полем.

LaTeX

$$$\operatorname{finrank}_K E = 1 \;\iff\; K = \top$$$

Lean4

theorem finrank_eq_one_iff_eq_top {K : IntermediateField F E} : Module.finrank K E = 1 ↔ K = ⊤ :=
  by
  refine ⟨?_, (· ▸ IntermediateField.finrank_top)⟩
  rw [← Subalgebra.bot_eq_top_iff_finrank_eq_one, ← top_le_iff, ← top_le_iff]
  intro H x _
  obtain ⟨x, rfl⟩ := @H x IntermediateField.mem_top
  exact x.2

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