hasEigenvector_toLin_diagonal — Mathlib

English

Basis vectors are eigenvectors of the associated diagonal linear operator.

Русский

Базисные векторы являются собственными векторами соответствующего диагонального линейного отображения.

LaTeX

$$$\\text{HasEigenvector}(\\text{toLin}_{b,b}(\\text{diagonal } d), d_i, b_i)$$$

Lean4

/-- Basis vectors are eigenvectors of associated diagonal linear operator. -/
theorem hasEigenvector_toLin_diagonal (d : n → R) (i : n) (b : Basis n R M) :
    HasEigenvector (toLin b b (diagonal d)) (d i) (b i) :=
  ⟨mem_eigenspace_iff.mpr <| by simp [diagonal], Basis.ne_zero b i⟩

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