toLinearMapₛₗ₂'_single — Mathlib

English

The linear equivalence between matrices and bilinear maps establishes a canonical bijection compatible with changes of bases.

Русский

Линейное эквивалентное соответствие между матрицами и билинейными отображениями задаёт каноническую биекцию, совместимую с заменой базисов.

LaTeX

$$$\text{Matrix } n m N_2 \cong \text{ Bilinear}(n,m;N_2)$ as linear spaces.$$

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

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