chore(LapMatrix): use Matrix.mulVecLin instead of toLin'

[urkud]

• use Matrix.mulVec instead of Matrix.toLin' _ _; this is the simp-normal form;
• use Matrix.mulVecLin _ instead of Matrix.toLin' _.

I'm working on applying these changes across the library, see #25012.

---

[github-actions]

PR summary f9ea33a8b5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ card_connectedComponent_eq_finrank_ker_mulVecLin_lapMatrix
+ lapMatrix_mulVec_eq_zero_iff_forall_adj
+ lapMatrix_mulVec_eq_zero_iff_forall_reachable
+ mem_ker_mulVecLin_lapMatrix_of_connectedComponent

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

The *ᵥ changes look like a clear win, as the simp-normal form, but I think the others need some explanation, and maybe make sense to apply mathlib-wide. Could you perhaps split the former, and make a new PR explaining the latter?

[urkud]

@eric-wieser I've opened a PR that aims to apply these changes everywhere.