charpoly_cfc_eq — Mathlib

English

For a Hermitian A and a real-valued function f, the characteristic polynomial of the matrix cfc f A equals the product of linear factors X − C(f(λ_i)) over all eigenvalues λ_i of A.

Русский

Для эрмитовой A и функции f характеристический многочлен матрицы cfc f A равен произведению линейных множителей X − C(f(λ_i)) по всем собственным значениям λ_i A.

LaTeX

$$(cfc f A).charpoly = ∏_i (X - C(f(hA.eigenvalues i)))$$

Lean4

theorem charpoly_cfc_eq (f : ℝ → ℝ) : (cfc f A).charpoly = ∏ i, (X - C (f (hA.eigenvalues i) : 𝕜)) :=
  by
  rw [cfc_eq hA f, IsHermitian.cfc, charpoly_mul_comm, ← mul_assoc]
  simp [charpoly_diagonal]

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