feat(LinearAlgebra): commutative semirings satisfy strong rank condition

[alreadydone]

Co-authored-by: Aristotle Harmonic aristotle-harmonic@harmonic.fun

Thanks to ChatGPT and Gemini for converting part of Yi-Jia Tan's paper into LaTeX, which served as solutions provided to Aristotle.

---

[github-actions]

PR summary 0bb58f289c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.Matrix.Nonsingular (new file)	1410

---

Declarations diff

+ Nonsingular
+ adjp_diag_last_eq_detp_sub
+ adjp_last_col_eq
+ adjp_mul_apply_eq
+ adjp_mul_apply_ne
+ augmented_good
+ detp_eq_of_eq_row
+ detp_eq_submatrix_equiv
+ detp_eq_zero_of_exists_row_eq_zero
+ detp_laplace_last_row
+ exists_mulVec_eq_of_bad_entry'
+ finNeLastEquiv
+ instance [Nontrivial R] : StrongRankCondition R
+ linearIndependent_col_iff
+ linearIndependent_col_of_nonsingular
+ nonsingular_iff_det_mem_nonZeroDivisors
+ nonsingular_of_linearIndependent
+ nonsingular_of_linearIndependent_col
+ not_linearIndependent_of_bad_entry
+ not_linearIndependent_of_smul_eq
+ witness_from_bad_submatrix

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.

[SnirBroshi]

Suggested change

	`|A|⁺` and `|A|⁻` are `A.detp 1` and `A.detp (-1)` respectively in mathlib (`Matrix.detp`).
	`|A|⁺` and `|A|⁻` are `A.detp 1` and `A.detp (-1)` respectively (`Matrix.detp`).

[SnirBroshi]

Since you're referencing the instance by name, I think it should be explicitly named rather than relying on the naming algorithm to be backwards compatible.