English
If A is Hermitian and nonzero, there exists a nonzero eigenvector v with a nonzero eigenvalue t such that Av = t v.
Русский
Если A эрмитова и ненулевая, существует ненулевой собственный вектор v и ненулевой действительный множитель t такой, что Av = t v.
LaTeX
$$$\\\\exists v \\\\neq 0, \\\\exists t \\\\neq 0: A v = t v$$$
Lean4
/-- A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue. -/
theorem exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) :
∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v := by
classical
have : hA.eigenvalues ≠ 0 := by
contrapose! h_ne
have := hA.spectral_theorem
rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0), diagonal_zero,
mul_zero, zero_mul] at this
obtain ⟨i, hi⟩ := Function.ne_iff.mp this
exact ⟨_, _, hi, hA.eigenvectorBasis.orthonormal.ne_zero i, hA.mulVec_eigenvectorBasis i⟩
