isometryOfOrthonormal_apply — Mathlib

English

For each i, the equivalence sends the i-th basis vector to the corresponding b' vector at index e(i).

Русский

Эквивалентность отправляет i-й элемент базиса в соответствующий вектор b' на индексе e(i).

LaTeX

$$$$ (b.equiv b' e)(b_i) = b'_{e(i)}. $$$$

Lean4

theorem isometryOfOrthonormal_apply (v : OrthonormalBasis (Fin 2) ℝ F) (z : ℂ) :
    Complex.isometryOfOrthonormal v z = z.re • v 0 + z.im • v 1 := by
  simp [Complex.isometryOfOrthonormal, ← v.sum_repr_symm]

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