toMatrix₂_symm — Mathlib

English

The symmetry between the bilinear-to-matrix and matrix-to-bilinear maps holds at the level of symmetries: the inverse correspondence respects swapping left and right actions.

Русский

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

LaTeX

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

Lean4

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

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