toLinearMap₂'Aux_single — Mathlib

English

The matrix representation of a bilinear map on basis delta elements yields the corresponding entry: f(e_i,e_j) = M_{ij}.

Русский

Значение билинейного отображения на пары базисных векторов равно элементу матрицы M_{ij}.

LaTeX

$$$f(e_i,e_j) = M_{ij}$$$

Lean4

theorem toLinearMap₂'Aux_single (f : Matrix n m N₂) (i : n) (j : m) :
    f.toLinearMap₂'Aux σ₁ σ₂ (Pi.single i 1) (Pi.single j 1) = f i j :=
  by
  rw [Matrix.toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  have :
    (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) • (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') = f i j :=
    by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]
  rw [← this]
  exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by aesop

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