maxGenEigenspace_toLin'_diagonal_eq_eigenspace

English

For a diagonal operator D = diag(d), the μ-generalized eigenspace coincides with the μ-eigenspace for every μ. In particular, maxGenEigenspace(D, μ) = eigenspace(D, μ).

Русский

Для диагонального оператора D = diag(d) для каждого μ выполняется, что μ-обобщённое собственное пространство совпадает с μ-собственным пространством: maxGenEigenspace(D, μ) = eigenspace(D, μ).

LaTeX

$$$$ \forall\mu\in R:\quad \maxGenEigenspace(\mathrm{diag}(d),\mu) = \mathrm{eigenspace}(\mathrm{diag}(d),\mu). $$$$

Lean4

@[simp]
theorem maxGenEigenspace_toLin'_diagonal_eq_eigenspace [IsDomain R] :
    maxGenEigenspace (diagonal d).toLin' μ = eigenspace (diagonal d).toLin' μ :=
  maxGenEigenspace_toLin_diagonal_eq_eigenspace d <| Pi.basisFun R n

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