k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.233405
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.233405
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
have h := collinear_iff_rank_le_one k s
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.233405
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.233405
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ Module.rank k { x // x ∈ vectorSpan k s } ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
rw [← finrank_eq_rank] at h
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.233405
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k { x // x ∈ vectorSpan k s }
h : Collinear k s ↔ ↑(finrank k { x // x ∈ vectorSpan k s }) ≤ 1
⊢ Collinear k s ↔ finrank k { x // x ∈ vectorSpan k s } ≤ 1
exact_mod_cast h