case hf
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Function.Injective ↑(eval K V)
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Function.Surjective (Submodule.comap (eval K V))
apply Submodule.comap_surjective_of_injective
case hf
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ker (eval K V) = ⊥
case hf
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Function.Injective ↑(eval K V)
rw [← LinearMap.ker_eq_bot]
no goals
case hf
K : Type u₁
V : Type u₂
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ker (eval K V) = ⊥
apply eval_ker K V