K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, HasEigenvalue f c
simp_rw [hasEigenvalue_iff_mem_spectrum]
no goals
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f