Commit 2025-12-19 08:36 51a72787

feat(LinearAlgebra): more on StrongRankCondition (#32194) Strong rank condition fails for R iff there is a copy of $R^{(\mathbb{N})}$ in some $R^n$, iff some $R^n$ has infinity rank, iff some $R^{n+1}$ has zero finrank. As consequences, if all $R^n$ are Noetherian or Artinian, then $R$ satisfies the strong rank condition. To prove the first equivalence, I redeveloped a version of the "tunnels and tailings" construction @jcommelin and @kim-em contributed to mathlib ~4 years ago and made it work for Semiring/AddCommMonoid. The original construction was deprecated in [#12076](https://github.com/leanprover-community/mathlib4/commit/5948566497f56e1432c52d65623f1bb3c3937159) by @acmepjz and later removed, though some docstrings still remain, and I think it's now time to remove it. Also add an instance that finite semirings satisfy the Orzech property (and therefore strong rank condition and invariant basis number).