English
The characteristic polynomial of a Hermitian matrix factors as a product of linear terms corresponding to its eigenvalues.
Русский
Характеристический многочлен эрмитовой матрицы распадается на произведение линейных множителей, соответствующих её собственным значениям.
LaTeX
$$$A.charpoly = \prod_i (X - \lambda_i)$, где $\lambda_i$ — eigenvalues$$
Lean4
theorem eigenvalues_eq (i : n) :
(hA.eigenvalues i) = RCLike.re (dotProduct (star ⇑(hA.eigenvectorBasis i)) (A *ᵥ ⇑(hA.eigenvectorBasis i))) :=
by
rw [dotProduct_comm]
simp only [mulVec_eigenvectorBasis, smul_dotProduct, ← EuclideanSpace.inner_eq_star_dotProduct,
inner_self_eq_norm_sq_to_K, RCLike.smul_re, hA.eigenvectorBasis.orthonormal.1 i, mul_one, algebraMap.coe_one,
one_pow, RCLike.one_re]
