English
If diagonal a is on the left, then kroneckerMap f diagonal(a) B equals a reindexed block diagonal built from B mapped by f along the a-diagonal entries.
Русский
Если диагональ слева задана как diagonal(a), то kroneckerMap f diagonal(a) B равняется переиндексированной блочной диагонали, состоящей из B, где каждый элемент обрабатывается f по диагональным индексам a.
LaTeX
$$$\operatorname{kroneckerMap} f (\mathrm{diagonal}\ a) B = \mathrm{reindex} (\mathrm{Equiv.prodComm}\ _\ _ ) (\mathrm{blockDiagonal}\ (\lambda i. B.map(\lambda b. f(a_i, b))))$$$
Lean4
theorem kroneckerMap_diagonal_left [Zero α] [Zero γ] [DecidableEq l] (f : α → β → γ) (hf : ∀ b, f 0 b = 0) (a : l → α)
(B : Matrix m n β) :
kroneckerMap f (diagonal a) B =
Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => B.map fun b => f (a i) b) :=
by
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]
