no goals
ι : Type ?u.40791
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
u v : ℙ K V
⊢ Independent ![u, v] ↔ u ≠ v
rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]