toMatrixOrthonormal_apply_apply — Mathlib

English

The (i,j)-entry of the matrix [f]_{v₁} is the inner product ⟪v₁ i, f(v₁ j)⟫ with respect to the orthonormal basis v₁.

Русский

Элемент матрицы [f]_{v₁} в позиции (i,j) равен скалярному произведению ⟪v₁ i, f(v₁ j)⟫ по базису v₁.

LaTeX

$$$[f]_{v_1}(i,j) = \langle v_1 i, f(v_1 j) \rangle$$$

Lean4

theorem toMatrixOrthonormal_apply_apply (f : E →ₗ[𝕜] E) (i j : n) : toMatrixOrthonormal v₁ f i j = ⟪v₁ i, f (v₁ j)⟫_𝕜 :=
  calc
    _ = v₁.repr (f (v₁ j)) i := f.toMatrix_apply ..
    _ = ⟪v₁ i, f (v₁ j)⟫_𝕜 := v₁.repr_apply_apply ..

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