This is part one of #12076.

`OrzechProperty R` is a type class stating that `R` satisfies the following property: for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective.

We stated some basic results about `OrzechProperty` and proved that it implies `StrongRankCondition`.

…erty` (#13425)

This is part 2 of #12076.

It states that if

- `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in <https://math.stackexchange.com/a/1066128>), or
- `R` is a commutative ring and `M` is a finitely generated `R`-module (based on the proof in <https://math.stackexchange.com/a/1066110>),

if `N` is a submodule of `M`, `f : N -> M` is a surjective `R`-module homomorphism, then it is also injective.

These results generalize `(IsNoetherian|Module.Finite).injective_of_surjective_endomorphism`.

The proof for Noetherian case uses `LinearMap.iterateMapComap` which is put into `Mathlib/Algebra/Module/Submodule/IterateMapComap.lean`.

The changed proof makes `LinearMap.tunnel` and `LinearMap.tailing` not used in any other parts of mathlib. Remove them or not is leaved for future discussion.

…endomorphism` and `commRing_strongRankCondition` (#12076)

- `Module.Finite.injective_of_surjective_endomorphism` is proved via `OrzechProperty.injective_of_surjective_endomorphism` since we already proved that commutative rings have `OrzechProperty`.
- `commRing_strongRankCondition` is proved via `inferInstance` since we know that commutative rings have `OrzechProperty`, and any nontrivial ring satisfying `OrzechProperty` also satisfies `StrongRankCondition`.

Due to the change of proof, some imports in the corresponding files become unnecessary, as reported by `shake`. This makes the change of imports in a lot of files.

The change of proof also makes `LinearMap.tunnel` and `LinearMap.tailing` not used in mathlib anymore.
These are marked as deprecated with no replacements.



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>

…erty` (#13425)

This is part 2 of #12076.

It states that if

- `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in <https://math.stackexchange.com/a/1066128>), or
- `R` is a commutative ring and `M` is a finitely generated `R`-module (based on the proof in <https://math.stackexchange.com/a/1066110>),

if `N` is a submodule of `M`, `f : N -> M` is a surjective `R`-module homomorphism, then it is also injective.

These results generalize `(IsNoetherian|Module.Finite).injective_of_surjective_endomorphism`.

The proof for Noetherian case uses `LinearMap.iterateMapComap` which is put into `Mathlib/Algebra/Module/Submodule/IterateMapComap.lean`.

The changed proof makes `LinearMap.tunnel` and `LinearMap.tailing` not used in any other parts of mathlib. Remove them or not is leaved for future discussion.

…endomorphism` and `commRing_strongRankCondition` (#12076)

- `Module.Finite.injective_of_surjective_endomorphism` is proved via `OrzechProperty.injective_of_surjective_endomorphism` since we already proved that commutative rings have `OrzechProperty`.
- `commRing_strongRankCondition` is proved via `inferInstance` since we know that commutative rings have `OrzechProperty`, and any nontrivial ring satisfying `OrzechProperty` also satisfies `StrongRankCondition`.

Due to the change of proof, some imports in the corresponding files become unnecessary, as reported by `shake`. This makes the change of imports in a lot of files.

The change of proof also makes `LinearMap.tunnel` and `LinearMap.tailing` not used in mathlib anymore.
These are marked as deprecated with no replacements.



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>

…erty` (#13425)

This is part 2 of #12076.

It states that if

- `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in <https://math.stackexchange.com/a/1066128>), or
- `R` is a commutative ring and `M` is a finitely generated `R`-module (based on the proof in <https://math.stackexchange.com/a/1066110>),

if `N` is a submodule of `M`, `f : N -> M` is a surjective `R`-module homomorphism, then it is also injective.

These results generalize `(IsNoetherian|Module.Finite).injective_of_surjective_endomorphism`.

The proof for Noetherian case uses `LinearMap.iterateMapComap` which is put into `Mathlib/Algebra/Module/Submodule/IterateMapComap.lean`.

The changed proof makes `LinearMap.tunnel` and `LinearMap.tailing` not used in any other parts of mathlib. Remove them or not is leaved for future discussion.

…endomorphism` and `commRing_strongRankCondition` (#12076)

- `Module.Finite.injective_of_surjective_endomorphism` is proved via `OrzechProperty.injective_of_surjective_endomorphism` since we already proved that commutative rings have `OrzechProperty`.
- `commRing_strongRankCondition` is proved via `inferInstance` since we know that commutative rings have `OrzechProperty`, and any nontrivial ring satisfying `OrzechProperty` also satisfies `StrongRankCondition`.

Due to the change of proof, some imports in the corresponding files become unnecessary, as reported by `shake`. This makes the change of imports in a lot of files.

The change of proof also makes `LinearMap.tunnel` and `LinearMap.tailing` not used in mathlib anymore.
These are marked as deprecated with no replacements.



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>

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).