[Merged by Bors] - feat(LinearAlgebra/Matrix/Adjugate): M.det = 0 if M *ᵥ v = 0 where v contains a non-zero-divisor

[SnirBroshi]

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.

---

The natural language proof is by ChatGPT 5.5; the rest is entirely human-made: the code, the counterexample, and also the idea for the statement.

[github-actions]

PR summary a7cb828610

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisors

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[b-mehta]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style