toLinearMap₂'_apply — Mathlib

English

The evaluation of a bilinear map on basis delta vectors recovers the matrix entries.

Русский

Оценка билинейного отображения на дельтовекторах базиса восстанавливает элементы матрицы.

LaTeX

$$$\text{For } M, x, y,\quad M_{ij} = f(e_i,e_j)$$$

Lean4

theorem toLinearMap₂'_apply (M : Matrix n m N₂) (x : n → S₁) (y : m → S₂) :
    -- porting note: we don't seem to have `∑ i j` as valid notation yet
    Matrix.toLinearMap₂' R M x y = ∑ i, ∑ j, x i • y j • M i j :=
  Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by rw [RingHom.id_apply, RingHom.id_apply, smul_comm]

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