English
The Kronecker product of two singleton matrices corresponds to the singleton product: single ia ja a ⊗ₖ single ib jb b = single ((ia, ib)) ((ja, jb)) (a b).
Русский
Кронекерово произведение двух единичных матриц даёт единичную матрицу размера пары индексов, со значением a·b.
LaTeX
$$$ \mathrm{single}_{ia,ja}(a) \otimes_k \mathrm{single}_{ib,jb}(b) = \mathrm{single}_{(ia,ib),(ja,jb)}(a b) $$$
Lean4
theorem single_kronecker_single [MulZeroClass α] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
(ia : l) (ja : m) (ib : n) (jb : p) (a b : α) :
single ia ja a ⊗ₖ single ib jb b = single (ia, ib) (ja, jb) (a * b) :=
kroneckerMap_single_single _ _ _ _ _ zero_mul mul_zero _ _