no goals
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ker (eval K V) = ⊥
classical exact (Basis.ofVectorSpace K V).eval_ker
no goals
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ker (eval K V) = ⊥
exact (Basis.ofVectorSpace K V).eval_ker