mulVec_eigenvectorBasis — Mathlib

English

Each eigenvector v_i of A with eigenvalue λ_i satisfies A v_i = λ_i v_i.

Русский

Каждый собственный вектор v_i эрмитовой матрицы удовлетворяет A v_i = λ_i v_i.

LaTeX

$$$A \cdot v_i = \lambda_i v_i$ for each eigenvector $v_i$ in the eigenvectorBasis.$$

Lean4

theorem mulVec_eigenvectorBasis (j : n) :
    A *ᵥ ⇑(hA.eigenvectorBasis j) = (hA.eigenvalues j) • ⇑(hA.eigenvectorBasis j) := by
  simpa only [eigenvectorBasis, OrthonormalBasis.reindex_apply, toEuclideanLin_apply,
    RCLike.real_smul_eq_coe_smul (K := 𝕜)] using
    congr(⇑$((isHermitian_iff_isSymmetric.1 hA).apply_eigenvectorBasis finrank_euclideanSpace
          ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm j)))

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