toLinearMap₂'_toMatrix' — Mathlib

English

The two-way passage between bilinear maps and matrices is involutive; applying converting maps back and forth yields the original object.

Русский

Двойной переход между билинейными формами и матрицами является инволютивным; преобразование туда и обратно возвращает исходный объект.

LaTeX

$$$\mathrm{toMatrix}_{\mathrm{sl}2}'(R) \text{ and } \mathrm{toLinearMap}_{\mathrm{sl}2}'(R, \sigma_1, \sigma_2)\text{ are mutual inverses.}$$$

Lean4

@[simp]
theorem toLinearMap₂'_toMatrix' (B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) :
    Matrix.toLinearMap₂' R (LinearMap.toMatrix₂' R B) = B :=
  (Matrix.toLinearMap₂' R).apply_symm_apply B

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