no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Submodule K V
inst✝ : FiniteDimensional K { x // x ∈ W }
⊢ finrank K { x // x ∈ W } ≤ 1 ↔ IsPrincipal W
rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, ← Cardinal.natCast_le, Nat.cast_one]