mathlib3

75207e91 - refactor(linear_algebra/eigenspace): refactor `eigenvectors_linearly_independent` (#10198)

refactor(linear_algebra/eigenspace): refactor `eigenvectors_linearly_independent` (#10198) This refactors the proof of the lemma ```lean lemma eigenvectors_linear_independent (f : End K V) (μs : set K) (xs : μs → V) (h_eigenvec : ∀ μ : μs, f.has_eigenvector μ (xs μ)) : linear_independent K xs ``` to extract the formulation ```lean lemma eigenspaces_independent (f : End K V) : complete_lattice.independent f.eigenspace ``` from which `eigenvectors_linear_independent` follows as a 1-liner. I don't need this for anything (although it might have applications -- for example, cardinality lemmas) -- just think it's a possibly more elegant statement.