no goals
m : Type u_1
R : Type ?u.16431
A : Type u_2
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : vecMul v M = 0
w : m → A
⊢ v ⬝ᵥ mulVec M w = 0
rw [dotProduct_mulVec, hv, zero_dotProduct]