toLinearMapₛₗ₂'_toMatrix' — Mathlib

English

For any bilinear map B, converting it to a matrix and back yields the same bilinear map: Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ (LinearMap.toMatrixₛₗ₂' R B) = B.

Русский

Для любого билинейного отображения B преобразование в матрицу и обратно дает то же самое билинейное отображение: Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ (LinearMap.toMatrixₛₗ₂' R B) = B.

LaTeX

$$$\mathrm{toLinearMap}_{\mathrm{sl}2}'(R, \sigma_1, \sigma_2) \bigl( \mathrm{toMatrix}_{\mathrm{sl}2}'(R) \ B \bigr) = B.$$$

Lean4

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

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