bot_eq_top_of_finrank_adjoin_eq_one

English

If every x ∈ E satisfies finrank F F⟮x⟯ = 1, then ⊥ = ⊤.

Русский

Если каждый x из E удовлетворяет finrank F F⟮x⟯ = 1, то нижнее и верхнее поля совпадают.

LaTeX

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

Lean4

theorem bot_eq_top_of_finrank_adjoin_eq_one (h : ∀ x : E, finrank F F⟮x⟯ = 1) : (⊥ : IntermediateField F E) = ⊤ :=
  by
  ext y
  rw [iff_true_right IntermediateField.mem_top]
  exact finrank_adjoin_simple_eq_one_iff.mp (h y)

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