mathlib3

c7ba3dd0 - refactor(linear_algebra/eigenspace): refactor exists_eigenvalue (#7345)

refactor(linear_algebra/eigenspace): refactor exists_eigenvalue (#7345) We replace the proof of `exists_eigenvalue` with the more general fact: ``` /-- Every element `f` in a nontrivial finite-dimensional algebra `A` over an algebraically closed field `K` has non-empty spectrum: that is, there is some `c : K` so `f - c • 1` is not invertible. -/ lemma exists_spectrum_of_is_alg_closed_of_finite_dimensional (𝕜 : Type*) [field 𝕜] [is_alg_closed 𝕜] {A : Type*} [nontrivial A] [ring A] [algebra 𝕜 A] [I : finite_dimensional 𝕜 A] (f : A) : ∃ c : 𝕜, ¬ is_unit (f - algebra_map 𝕜 A c) := ... ``` We can then use this fact to prove Schur's lemma. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>