English
If f is bilinear with f(0, b)=0 and f(a, 0)=0, then kroneckerMap f diagonal(a) diagonal(b) equals the diagonal with entries f(a_i, b_j) at position (i,j).
Русский
Если f билинейна и выполняет f(0,b)=0, f(a,0)=0, то kroneckerMap f diagonal(a) diagonal(b) даёт диагональ, чьи элементы равны f(a_i, b_j) на позиции (i,j).
LaTeX
$$$\operatorname{kroneckerMap} f (\mathrm{diagonal}\ a) (\mathrm{diagonal}\ b) = \mathrm{diagonal}\big( \lambda mn. f(a_{mn.1}, b_{mn.2}) \big)$$$
Lean4
theorem kroneckerMap_diagonal_diagonal [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n] (f : α → β → γ)
(hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : m → α) (b : n → β) :
kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2) :=
by
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]
