bot_eq_top_of_rank_adjoin_eq_one — Mathlib

English

If for all x ∈ E we have rank F F⟮x⟯ = 1, then ⊥ = ⊤.

Русский

Если для каждого x ∈ E размерность F⟮x⟯ над F равна 1, то нижнее и верхнее поля совпадают.

LaTeX

$$(∀ x : E, \operatorname{rank} F F⟮x⟯ = 1) → (⊥ : IntermediateField F E) = ⊤$$

Lean4

/-- If `F⟮x⟯` has dimension `1` over `F` for every `x ∈ E` then `F = E`. -/
theorem bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) : (⊥ : IntermediateField F E) = ⊤ :=
  by
  ext y
  rw [iff_true_right IntermediateField.mem_top]
  exact rank_adjoin_simple_eq_one_iff.mp (h y)

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