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"](leanprover-community/mathlib3@86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) 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](5948566) 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).

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"](leanprover-community/mathlib3@86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) 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](5948566) 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).

…y#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"](leanprover-community/mathlib3@86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) construction @jcommelin and @kim-em contributed to mathlib ~4 years ago and made it work for Semiring/AddCommMonoid. The original construction was deprecated in [leanprover-community#12076](leanprover-community@5948566) 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).

…y#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"](leanprover-community/mathlib3@86766851#diff-7829719aad6a9e3e617da2a7cf29dba4d55516b27e18f240eca352f4983d67b7R472-R491) construction @jcommelin and @kim-em contributed to mathlib ~4 years ago and made it work for Semiring/AddCommMonoid. The original construction was deprecated in [leanprover-community#12076](leanprover-community@5948566) 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).