adjoin_simple_eq_bot_iff — Mathlib

English

For any element α in E, the intermediate field generated by α over F is the bottom field exactly when α lies in the bottom field.

Русский

Для любого элемента α в E подполе, порождаемое α над F, равно ⊥ тогда, когда α ∈ ⊥.

LaTeX

$$$F\langle \alpha \rangle = \bot \iff \alpha \in (\bot : \text{IntermediateField } F E)$$$

Lean4

theorem adjoin_simple_eq_bot_iff : F⟮α⟯ = ⊥ ↔ α ∈ (⊥ : IntermediateField F E) := by simp

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