toLin_transpose — Mathlib

English

For any M, the transpose relation between matrix representations and linear maps holds under dual bases.

Русский

Для любого M справедливо отношение между матричным представлением и линейным отображением через пары базисов дуальных.

LaTeX

$$toLin^{\,dual} transfer equals transpose of toLin$$

Lean4

@[simp]
theorem toLin_transpose (M : Matrix ι₁ ι₂ K) :
    Matrix.toLin B₁.dualBasis B₂.dualBasis Mᵀ = Module.Dual.transpose (R := K) (Matrix.toLin B₂ B₁ M) :=
  by
  apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective
  rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]

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