chore: remove redundant lemma LinearMap.IsSymmetric.eigenspace_invariant_of_commute

[ocfnash]

---

I noticed that #15012 seemed to prove a few results with unnecessarily strong assumptions (mostly, working over ℝ or ℂ when any commutative ring would suffice). I don't have time to generalise it all but I thought I'd highlight this observation with this small PR.

[github-actions]

PR summary 5ae32b7ca0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- eigenspace_invariant_of_commute

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[JonBannon]

This is amazing, Oliver. Jireh just suggested that I remove that lemma and make this fix using generalized eigenspaces. Thanks!

[JonBannon]

Thanks!!

[JonBannon]

Also, thanks for the suggestion about the commutative rings. We are finishing up a PR for finite tuples and will fold in the weakened assumptions throughout with that PR.

[ocfnash]

Great news! Thanks so much @JonBannon 🎉

[j-loreaux]

Thanks! I think we'll just fold these suggestions (and the generalization to CommRing) into #16569, and thereby avoid the merge conflict. I'm closing this for that reason.