no goals
R : Type u_2
inst✝¹ : CommSemiring R
k : Type ?u.306834
l : Type ?u.306837
m : Type ?u.306840
n : Type u_1
inst✝ : Fintype n
M : Matrix n n R
⊢ ker (mulVecLin M) = ⊥ ↔ ∀ (v : n → R), mulVec M v = 0 → v = 0
simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]