no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)
rw [linearIndependent_iff_card_eq_finrank_span, finrank_range_le_card.le_iff_eq]