toMatrix_transpose_apply — Mathlib

English

The transpose of the matrix representing f encodes the coordinates of f(v1(j)) in the basis v2, i.e. its jth column (or row, depending on orientation) equals those coordinates.

Русский

Транспонированная матрица, представляющая f, кодирует координаты f(v1(j)) в базисе v2: j-ая колонка совпадает с этими координатами.

LaTeX

$$$\\big(\\text{LinearMap.toMatrix } v_1 v_2 f\\big)^{\\mathrm{T}}_{j} = v_2.repr\\big(f(v_1 j)\\big)$$$

Lean4

theorem toMatrix_transpose_apply (f : M₁ →ₗ[R] M₂) (j : n) : (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j)) :=
  funext fun i ↦ f.toMatrix_apply _ _ i j

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