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
⊢ ⊥ = ⊤ ↔ finrank F E = 1
rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
  Subalgebra.finrank_eq_one_iff, eq_comm]