toLinearMap₂' — Mathlib

English

The action of a bilinear map on basis-driven arguments matches the matrix entry formula.

Русский

Действие билинейного отображения на базисных аргументах даёт формулу элемента матрицы.

LaTeX

$$$\text{For } M, x, y, \; M \mapsto f, \; f(e_i,e_j) = M_{ij}$$$

Lean4

/-- The linear equivalence between `n × n` matrices and bilinear maps on `n → R` -/
def toLinearMap₂' : Matrix n m N₂ ≃ₗ[R] (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂ :=
  (LinearMap.toMatrix₂' R).symm

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