eigenvectorUnitary_mulVec — Mathlib

English

The eigenvectorUnitary acts on a standard basis vector to yield the corresponding eigenvector.

Русский

EigenvectorUnitary применяет к базисному вектору, получая соответствующий собственный вектор.

LaTeX

$$$eigenvectorUnitary(h_A) *^{\!} \mathbf{e}_{j} = v_j$$$

Lean4

theorem eigenvectorUnitary_mulVec (j : n) : eigenvectorUnitary hA *ᵥ Pi.single j 1 = ⇑(hA.eigenvectorBasis j) := by
  simp_rw [mulVec_single_one, eigenvectorUnitary_col_eq]

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