English
There is a canonical bijection between bilinear maps on basis vectors and matrices: a bilinear map f corresponds to a matrix whose (i,j) entry is f(e_i, f_j).
Русский
Существует каноническое биекция между билинейными отображениями на базисах и матрицами: отображение f соответствует матрице с элементом (i,j) равным f(e_i, e_j).
LaTeX
$$$f \mapsto [f(e_i,e_j)]_{i,j}$ gives a bijection between bilinear maps and matrices.$$
Lean4
/-- The map from `Matrix n n R` to bilinear maps on `n → R`.
This is an auxiliary definition for the equivalence `Matrix.toLinearMap₂'`. -/
def toLinearMap₂'Aux (f : Matrix n m N₂) : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂ :=
-- porting note: we don't seem to have `∑ i j` as valid notation yet
mk₂'ₛₗ σ₁ σ₂ (fun (v : n → R₁) (w : m → R₂) => ∑ i, ∑ j, σ₂ (w j) • σ₁ (v i) • f i j)
(fun _ _ _ => by simp only [Pi.add_apply, map_add, smul_add, sum_add_distrib, add_smul])
(fun c v w => by
simp only [Pi.smul_apply, smul_sum, smul_eq_mul, σ₁.map_mul, ← smul_comm _ (σ₁ c), MulAction.mul_smul])
(fun _ _ _ => by simp only [Pi.add_apply, map_add, add_smul, sum_add_distrib])
(fun _ v w => by simp only [Pi.smul_apply, smul_eq_mul, map_mul, MulAction.mul_smul, smul_sum])
