no goals
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ finrank K V = 1 ↔ ∃ v _n, ∀ (w : V), ∃ c, c • v = w
rw [finrank_eq_one_iff PUnit.{u+1}, Basis.basis_singleton_iff PUnit]