Commit 2020-08-28 16:07 4ccbb514

feat(linear_algebra): eigenspaces of linear maps (#3927) Add eigenspaces and eigenvalues of linear maps. Add lemma that in a finite-dimensional vector space over an algebraically closed field, eigenvalues exist. Add lemma that eigenvectors belonging to distinct eigenvalues are linearly independent. This is a rework of #3864, following Cyril's suggestion. Generalized eigenspaces will come in a subsequent PR.