toMatrix_transpose — Mathlib

English

For M, the matrix corresponding to the transpose of a linear map equals the transpose of the matrix of the original map.

Русский

Матрица, соответствующая транспонированию линейного отображения, равна транспонированной матрице исходного отображения.

LaTeX

$$Matrix.toLin B_1.dualBasis B_2.dualBasis M^T = (Matrix.toLin B_2 B_1 M)^T$$

Lean4

@[simp]
theorem toMatrix_transpose (u : V₁ →ₗ[K] V₂) :
    LinearMap.toMatrix B₂.dualBasis B₁.dualBasis (Module.Dual.transpose (R := K) u) = (LinearMap.toMatrix B₁ B₂ u)ᵀ :=
  by
  ext i j
  simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr, B₂.dualBasis_apply,
    Matrix.transpose_apply, LinearMap.comp_apply]

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