English
There is a canonical inverse correspondence between n-by-m matrices over N2 and bilinear maps represented by linear maps with respect to σ1 and σ2. In particular, the inverse of the matrix-to-bilinear-map identification is exactly the bilinear-to-matrix identification given by Matrix.toLinearMapₛₗ₂'.
Русский
Существует каноническое обратное соответствие между матрицами размерности n×m над N₂ и билинейными отображениями, представляемыми линейными отображениями относительно σ₁ и σ₂. В частности, обратное от сопоставления матрица→би-линейное отображение равно сопоставлению билинейное отображение→матрица, заданному Matrix.toLinearMapₛₗ₂'.
LaTeX
$$$\bigl(\mathrm{toMatrix}_{\mathrm{sl} 2}'(R)\bigr)^{-1} = \mathrm{toLinearMap}_{\mathrm{sl} 2}'(R, \sigma_1, \sigma_2).$$$
Lean4
@[simp]
theorem toMatrixₛₗ₂'_symm :
((LinearMap.toMatrixₛₗ₂' R).symm : Matrix n m N₂ ≃ₗ[R] _) = Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ :=
rfl
