eigenvalues_eq_zero_iff — Mathlib

English

The eigenvalues of a Hermitian matrix are all zero if and only if the matrix is zero.

Русский

Собственные значения эрмитовой матрицы все нули тогда и только тогда, когда матрица равна нулю.

LaTeX

$$$ h_A\\\\,\\\\mathrm{eigenvalues} = 0 \\\\iff A = 0$$$

Lean4

/-- The eigenvalues of a Hermitian matrix `A` are all zero iff `A = 0`. -/
theorem eigenvalues_eq_zero_iff : hA.eigenvalues = 0 ↔ A = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by ext; simp [h, eigenvalues_eq]⟩
  rw [hA.spectral_theorem, h, Pi.comp_zero, RCLike.ofReal_zero, Function.const_zero, Pi.zero_def, diagonal_zero,
    mul_zero, zero_mul]

Похожие утверждения