toMatrix₂_basisFun — Mathlib

English

The two-way correspondences between matrix representations and bilinear maps extend to the two-variable case, preserving the bilinear form structure.

Русский

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

LaTeX

$$$\mathrm{toMatrix}_{2}' (R) (B) \mapsto B$ and $B \mapsto \mathrm{toLinearMap}_{2}'(R) (B)$ are inverses.$$

Lean4

theorem toMatrix₂_basisFun :
    LinearMap.toMatrix₂ (Pi.basisFun R n) (Pi.basisFun R m) = LinearMap.toMatrix₂' R (N₂ := N₂) :=
  by
  ext B
  rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂'_apply, Pi.basisFun_apply, Pi.basisFun_apply]

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