English
The map sending a bilinear form to its matrix with respect to chosen bases is a linear isomorphism between bilinear maps and matrices.
Русский
Отображение билинейной формы в матрицу по выбранным базисам есть линейное изоморфизм между билинейными отображениями и матрицами.
LaTeX
$$$\text{Bilin}(n,m;N_2) \cong M_{n,m}(N_2)$ as linear spaces.$$
Lean4
/-- The linear map from sesquilinear maps to `Matrix n m N₂` given an `n`-indexed basis for `M₁`
and an `m`-indexed basis for `M₂`.
This is an auxiliary definition for the equivalence `Matrix.toLinearMapₛₗ₂'`. -/
def toMatrix₂Aux (b₁ : n → M₁) (b₂ : m → M₂) : (M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) →ₗ[R] Matrix n m N₂
where
toFun f := of fun i j => f (b₁ i) (b₂ j)
map_add' _f _g := rfl
map_smul' _f _g := rfl
