toMatrix'_toLinearMapₛₗ₂' — Mathlib

English

The inverse relations K ↦ Matrix(K) and Matrix ↦ K are identity on the appropriate domain; i.e., composing these canonical maps yields the original bilinear map or matrix.

Русский

Обратные соотношения сохраняют идентичность: композиция канонических отображений даёт исходное билинейное отображение или матрицу.

LaTeX

$$$\bigl(\mathrm{toMatrix}_{\mathrm{sl}2}'(R)\bigr)^{\!-1} = \mathrm{toLinearMap}_{\mathrm{sl}2}'(R, \sigma_1, \sigma_2) \quad\text{and}\quad \bigl(\mathrm{toLinearMap}_{\mathrm{sl}2}'(R, \sigma_1, \sigma_2)\bigr)^{\!-1} = \mathrm{toMatrix}_{\mathrm{sl}2}'(R).$$$

Lean4

@[simp]
theorem toMatrix'_toLinearMapₛₗ₂' (M : Matrix n m N₂) :
    LinearMap.toMatrixₛₗ₂' R (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ M) = M :=
  (LinearMap.toMatrixₛₗ₂' R).apply_symm_apply M

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