toLinearMap₂_symm — Mathlib

English

Duality between linear maps and matrices yields a symmetric relation between the correspondences on both sides of the bilinear pairing.

Русский

Двойственность между линейными отображениями и матрицами даёт симметричное отношение между соответствиями по обе стороны билинейной пары.

LaTeX

$$$\mathrm{toLinearMap}_{\mathrm{sl}2}'(R)^{\mathrm{symm}} = \mathrm{toMatrix}_{\mathrm{sl}2}'(R).$$$

Lean4

@[simp]
theorem toLinearMap₂_symm : (Matrix.toLinearMap₂ b₁ b₂).symm = LinearMap.toMatrix₂ (N₂ := N₂) b₁ b₂ :=
  (LinearMap.toMatrix₂ b₁ b₂).symm_symm

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