no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
S : Submodule K V
inst✝ : FiniteDimensional K { x // x ∈ S }
⊢ finrank K { x // x ∈ S } = 0 ↔ S = ⊥
rw [← rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Cardinal.natCast_inj]