English
The Kronecker product I_m ⊗ B is, up to a permutation of indices, the block-diagonal matrix whose blocks are all copies of B.
Русский
Кронекерово произведение I_m ⊗ B является, после перестановки индексов, блочно-диагональной матрицей, состоящей из копий B.
LaTeX
$$$$ I_m \\otimes B = \\operatorname{reindex}(\\text{Equiv.prodComm}, \\text{Equiv.prodComm})\\big(\\operatorname{blockDiagonal}(\\lambda _ \\mapsto B)\\big) $$$$
Lean4
theorem one_kronecker [MulZeroOneClass α] [DecidableEq l] (B : Matrix m n α) :
(1 : Matrix l l α) ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun _ => B) :=
(diagonal_kronecker _ _).trans <| congr_arg _ <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => one_mul _
