K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Submodule.span K {Projectivization.rep v} } = 1
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Projectivization.submodule v } = 1
rw [submodule_eq]
no goals
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Submodule.span K {Projectivization.rep v} } = 1
exact finrank_span_singleton v.rep_nonzero