feat(LinearAlgebra/Matrix/Adjugate): M.det = 0 if M *ᵥ v = 0 where v contains a non-zero-divisor (leanprover-community#39642)

The non-zero-divisor requirement is necessary since otherwise we could take any `a * b = 0` with `a ≠ 0 ∧ b ≠ 0` and consider the 1x1 matrix formed by `a` and the single-entry vector formed by `b`. Then `M.det = a ≠ 0` and `M *ᵥ v = a * b = 0`.

Author: SnirBroshi

Mathlib/LinearAlgebra/Matrix/Adjugate.lean

@@ -284,6 +284,11 @@ divides `b`. -/
 theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b := by
   rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]
 
+theorem det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisors {M : Matrix n n α} {v : n → α}
+    (h : M *ᵥ v = 0) {i : n} (hi : v i ∈ nonZeroDivisors α) : M.det = 0 := by
+  apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp
+  simpa [adjugate_mul, smul_mulVec] using congr((M.adjugate *ᵥ $h) i)
+
 theorem adjugate_subsingleton [Subsingleton n] (A : Matrix n n α) : adjugate A = 1 := by
   ext i j
   simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]