Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-10 07:43 8e9b1f0f

View on Github →

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.

Estimated changes