eigenvalues_eq_eigenvalues_iff — Mathlib

English

Two Hermitian matrices have the same eigenvalues if and only if they have the same characteristic polynomial.

Русский

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

LaTeX

$$$h_A.\text{eigenvalues} = h_B.\text{eigenvalues} \;\Longleftrightarrow\; A.charpoly = B.charpoly$$$

Lean4

theorem eigenvalues_eq_eigenvalues_iff : hA.eigenvalues = hB.eigenvalues ↔ A.charpoly = B.charpoly :=
  by
  constructor <;> intro h
  · rw [hA.charpoly_eq, hB.charpoly_eq, h]
  · suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]
    simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]

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