[Merged by Bors] - feat: generalized eigenspaces are independent

[ocfnash]

The main change is to upgrade the existing Module.End.eigenspaces_independent, which applied only to eigenspaces (and required a [Field K] assumption) to Module.End.independent_generalizedEigenspace, which applies to generalized eigenspaces (and requires only [NoZeroSMulDivisors R M])

---

Split out from #7963

[j-loreaux]

This is the not the definition I was expecting for IsTriangularizable. Instead, I was expecting: "there exists a maximal chain of invariant subspaces". Over a finite dimensional vector space over a field, the definitions coincide, but not in the infinite dimensional setting. Thoughts?

[ocfnash]

This is the not the definition I was expecting for IsTriangularizable. Instead, I was expecting: "there exists a maximal chain of invariant subspaces". Over a finite dimensional vector space over a field, the definitions coincide, but not in the infinite dimensional setting. Thoughts?

Great point, I should have thought of this myself! I'm already yak shaving to some extent so I'm not sure if I have the appetite to develop the full theory at the moment. A reasonable compromise might be keep these results without taking ownership of the IsTriangularizable name.

Given your remarks, I'll split this PR in two: I think the results about independence should be less controversial.

[j-loreaux]

Looks pretty nice! Minor comments.

[j-loreaux]

I pushed a small golf. Feel free to revert if you prefer. Merge once CI passes.

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]

Pull request successfully merged into master.

Build succeeded:

• Check all files imported
• Lint style
• Build