[Merged by Bors] - feat: in finite dimensions, if a linear endomorphism is triangularizable, so is its restriction to any invariant submodule

[ocfnash]

---

Split out from #7963

• depends on: [Merged by Bors] - feat: generalized eigenspaces are independent #8177

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: generalized eigenspaces are independent #8177
  By Dependent Issues (🤖). Happy coding!

[ocfnash]

I note the following request to reviewers from @semorrison on Zulip:

if you see a PR that is renaming a file, but git does not report it as a rename (because too much stuff
was changed at the same time), can we please ask the author to make separate PRs doing the rename
and making the changes?

Renames that are not detected as renames are very likely to break nightly-testing. (Thanks to Matthew
Ballard for salvaging one such breakage overnight.)

Thus if the proposed rename in this PR is accepted, we should not merge this PR directly but split out
a rename-only PR first. I will wait for review before I make such a split.

[jcommelin]

I would like to see the renaming PR (-;

[ocfnash]

I would like to see the renaming PR (-;

Created here #8318

[jcommelin]

bors d+

[mathlib-bors]

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

[ocfnash]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Check all files imported
• Lint style
• Build