F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
⊢ Insert.insert ∅ α ⊆ ↑⊥ ↔ α ∈ ⊥
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
⊢ finrank F { x // x ∈ F⟮α⟯ } = 1 ↔ α ∈ ⊥
rw [finrank_adjoin_eq_one_iff]
no goals
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
S : Set E
K L : IntermediateField F E
⊢ Insert.insert ∅ α ⊆ ↑⊥ ↔ α ∈ ⊥
exact Set.singleton_subset_iff