k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.243973
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Module.rank k { x // x ∈ ⊥ } ≤ 1
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.243973
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅
rw [collinear_iff_rank_le_one, vectorSpan_empty]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.243973
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Module.rank k { x // x ∈ ⊥ } ≤ 1
simp