toMatrix₂Aux_toLinearMap₂'Aux

English

There is a canonical isomorphism between the space of bilinear maps and the space of n×m matrices given by (toMatrix₂Aux) and (toLinearMap₂'Aux).

Русский

Существует каноническое изоморфное отображение между билинейными отображениями и матрицами размерности n×m, заданное через toMatrix₂Aux и toLinearMap₂'Aux.

LaTeX

$$$\text{Bilin}(n,m;N_2) \cong M_{n,m}(N_2)$$$

Lean4

theorem toMatrix₂Aux_toLinearMap₂'Aux (f : Matrix n m N₂) :
    LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) (fun j => Pi.single j 1) (f.toLinearMap₂'Aux σ₁ σ₂) = f :=
  by
  ext i j
  simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]

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