hasEigenvector_toLin'_diagonal — Mathlib

English

The iSup of the eigen spaces of a diagonal operator equals the top subspace.

Русский

Супремум по iSup эйгенпространств диагонального оператора равен верхнему подпространству.

LaTeX

$$$iSup_{\\mu} \\; E_{\\mu}( (diagonal d).toLin b b ) = \\top$$$

Lean4

/-- Standard basis vectors are eigenvectors of any associated diagonal linear operator. -/
theorem hasEigenvector_toLin'_diagonal (d : n → R) (i : n) :
    HasEigenvector (toLin' (diagonal d)) (d i) (Pi.basisFun R n i) :=
  hasEigenvector_toLin_diagonal _ _ (Pi.basisFun R n)

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