English
For a Nat a and B, kronecker with a.cast equals a reindexed blockDiagonal of a • B.
Русский
Для натурального a матрица a.cast вкладывается в перестановку индексов по блочно-диагональной структуре.
LaTeX
$$$ \operatorname{kroneckerMap} (\dots) a.cast B = \operatorname{reindex} (\dots) (\operatorname{blockDiagonal} (\lambda x, a \cdot B)) $$$
Lean4
theorem natCast_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) (B : Matrix m n α) :
(a : Matrix l l α) ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => a • B) :=
diagonal_kronecker _ _ |>.trans <| by
congr! 2
ext
simp [(Nat.cast_commute a _).eq]