toMatrix₂'_apply — Mathlib

English

For a bilinear map B, converting it to a matrix via LinearMap.toMatrix₂' and then back via Matrix.toLinearMap₂' returns the original map: (toLinearMap₂' R σ₁ σ₂) (toMatrix₂' R B) = 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 toMatrix₂'_apply (B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂) (i : n) (j : m) :
    LinearMap.toMatrix₂' R B i j = B (Pi.single i 1) (Pi.single j 1) :=
  rfl

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