English
If A is any matrix and b is a diagonal matrix, then kroneckerMap f A diag(b) equals a block diagonal matrix whose blocks are A mapped entrywise by f with b’s diagonal entries.
Русский
Если A произвольна, а diag(b) — диагональная матрица, то kroneckerMap f A diag(b) равняется блочно-диагональной матрице, где каждый блок получается путём применения f к элементам A и диагональным элементам b.
LaTeX
$$$\operatorname{kroneckerMap} f A (\mathrm{diagonal}\ b) = \mathrm{blockDiagonal}\big( \lambda i. A.map(\lambda a. f(a, b_i)) \big)$$$
Lean4
theorem kroneckerMap_diagonal_right [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ) (hf : ∀ a, f a 0 = 0)
(A : Matrix l m α) (b : n → β) : kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i) :=
by
ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]
