K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
⊢ (∀ (φ : Dual K V), ↑φ v = 0) ↔ ∀ (x : Dual K V), ↑(↑(eval K V) v) x = ↑0 x
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
⊢ (∀ (φ : Dual K V), ↑φ v = 0) ↔ v = 0
rw [← eval_apply_eq_zero_iff K v, LinearMap.ext_iff]
no goals
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
⊢ (∀ (φ : Dual K V), ↑φ v = 0) ↔ ∀ (x : Dual K V), ↑(↑(eval K V) v) x = ↑0 x
rfl