feat(linear_algebra): add `restrict` for endomorphisms (#4053)
Add a `restrict` function for endomorphisms. Add some lemmas about the new function, including one about generalized eigenspaces. Add some additional lemmas about `linear_map.comp` that I do not use in the final proof, but still consider useful.
