eigenvectorUnitary_apply

Mathlib.LinearAlgebra.Matrix.Spectrum

URI: https://scilib.ai/kg/mathlib#Matrix.IsHermitian.eigenvectorUnitary_apply

English

The i-th row of eigenvectorUnitary corresponds to the i-th eigenvector coordinates.

Русский

i-я строка eigenvectorUnitary соответствует координатам i-го собственного вектора.

LaTeX

$$$\bigl(\text{eigenvectorUnitary}(h_A)\bigr)_{i,\cdot} = (h_A.\text{eigenvectorBasis} \; j)_{i}$$$

Lean4

@[simp]
theorem eigenvectorUnitary_apply (i j : n) : eigenvectorUnitary hA i j = ⇑(hA.eigenvectorBasis j) i :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru