feat: Generalize corollaries of rank-nullity theorem.

[erdOne]

---

[riccardobrasca]

@erdOne are you still interested in working on this PR? Or is it obsolete now?

[erdOne]

I'm busy until mid-March. I think I'll come back to this after that. Feel free to adopt if this is needed elsewhere.

[riccardobrasca]

Can you add a description of the PR?

Also, is it possible to split it? Correct me if I am wrong, but I have the impression you both generalize/move current results and add a new class. Maybe these two things are intertwined and difficult to separate, so don't worry if it is too much work to do it.

[erdOne]

I tried a bit and it seems hard to separate them.

[riccardobrasca]

I tried a bit and it seems hard to separate them.

OK, don't worry.

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit b3998cd8727de70280a0072a5767c3c8e03f0fdc. There were significant changes against commit 92c745e2994217861e83a6e65a6ee286dd6f5cd6:

  Benchmark                                       Metric         Change
  =====================================================================
+ ~Mathlib.Algebra.Module.PID                     instructions    -5.1%
- ~Mathlib.LinearAlgebra.Dimension.Finite         instructions    22.3%
- ~Mathlib.LinearAlgebra.Dimension.Localization   instructions    58.9%

[riccardobrasca]

Here are the benchmark results for commit b3998cd. There were significant changes against commit 92c745e:

  Benchmark                                       Metric         Change
  =====================================================================
+ ~Mathlib.Algebra.Module.PID                     instructions    -5.1%
- ~Mathlib.LinearAlgebra.Dimension.Finite         instructions    22.3%
- ~Mathlib.LinearAlgebra.Dimension.Localization   instructions    58.9%

@mattrobball do you think this is ok?

[erdOne]

Both file got longer (the +50％ file doubled in size) so I guess it's fine as long as downstream files aren't slowed?

[mattrobball]

Overall it is not terrible but it would nice to take a quick look at those two files to make sure you cannot make an easy change to fix the issue.

[mattrobball]

After actually looking at the changes, this is perfectly fine.

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors[bot]]

:v: erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[sgouezel]

bors r- Can you merge master and fix the build before sending it back to bors? bors d+

[mathlib-bors[bot]]

:v: erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors[bot]]

Canceled.

[erdOne]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style