no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.272580
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ AffineIndependent k p ↔ ¬Collinear k (Set.range p)
rw [collinear_iff_finrank_le_one,
  affineIndependent_iff_not_finrank_vectorSpan_le k p (Fintype.card_fin 3)]