toMatrix_transpose_apply' — Mathlib

English

For fixed bases, applying toLin to the matrix of a linear map f recovers f; i.e., Matrix.toLin v1 v2 (LinearMap.toMatrix v1 v2 f) = f.

Русский

Для фиксированных базисов применение toLin к матрице линейного отображения f восстанавливает f: Matrix.toLin v1 v2 (LinearMap.toMatrix v1 v2 f) = f.

LaTeX

$$$\\text{Matrix.toLin } v_1 v_2 (\\text{LinearMap.toMatrix } v_1 v_2 f) = f.$$$

Lean4

theorem toMatrix_transpose_apply' (f : M₁ →ₗ[R] M₂) (j : n) : (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j)) :=
  LinearMap.toMatrix_transpose_apply v₁ v₂ f j

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