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.
