no goals
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
h : LinearIndependent K b
⊢ Fintype.card ι ≤ finrank K V
simpa using cardinal_mk_le_finrank_of_linearIndependent h