toLinearMap₂'_single — Mathlib

English

The simple form of the linear equivalence between matrices and bilinear maps uses standard basis to recover entries straightforwardly.

Русский

Простая форма эквивалентности между матрицами и билинейными отображениями восстанавливает элементы по базису напрямую.

LaTeX

$$$\text{toLinearMap₂' }(M) = \text{bilinear map with } (i,j)\text{ entry } M_{ij}$$$

Lean4

@[simp]
theorem toLinearMap₂'_single (M : Matrix n m N₂) (i : n) (j : m) :
    Matrix.toLinearMap₂' R M (Pi.single i 1) (Pi.single j 1) = M i j :=
  Matrix.toLinearMap₂'Aux_single _ _ M i j

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