toLinearMap₂_toMatrix₂ — Mathlib

English

The map that takes a bilinear map to a matrix and the map that recovers a bilinear map from a matrix are inverse to each other when viewed through the standard basis couverture.

Русский

Отображение, переводящее билинейное отображение в матрицу, и обратное отображение обратно равны по стандартному базисному превращению.

LaTeX

$$$\mathrm{Matrix.toLinearMap₂}(b_1,b_2)\circ \mathrm{LinearMap.toMatrix₂}(b_1,b_2) = \mathrm{Id}$ and the dual equality.$$

Lean4

@[simp]
theorem toLinearMap₂_toMatrix₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
    Matrix.toLinearMap₂ b₁ b₂ (LinearMap.toMatrix₂ b₁ b₂ B) = B :=
  (Matrix.toLinearMap₂ b₁ b₂).apply_symm_apply B

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