K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ span K {v} = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w
rw [finrank_eq_one_iff_of_nonzero v nz]
no goals
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ span K {v} = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
apply span_singleton_eq_top_iff