no goals
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : Algebra F E
inst✝ : Nontrivial E
⊢ ⊥ = ⊤ ↔ Module.rank F E = 1
rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]