mathlib3
b2e881b9 - feat(linear_algebra/eigenspace): the eigenvalues of a linear endomorphism are in its spectrum (#10912)

Commit
4 years ago
feat(linear_algebra/eigenspace): the eigenvalues of a linear endomorphism are in its spectrum (#10912) This PR shows that the eigenvalues of `f : End R M` are in `spectrum R f`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Author
Parents
Loading