English
The Kronecker product of a matrix with a diagonal matrix equals a block-diagonal matrix with blocks given by A.map(a ⊗ b_i).
Русский
Кронекерово произведение матрицы с диагональной матрицей образует блочно-диагональную матрицу, состоящую из блоков A.map( a ⊗ b_i ).
LaTeX
$$A ⊗ₖₜ[R] diagonal b = blockDiagonal (λ i, A.map (λ a, a ⊗ₜ b i))$$
Lean4
theorem kroneckerTMul_diagonal [DecidableEq n] (A : Matrix l m α) (b : n → β) :
A ⊗ₖₜ[R] diagonal b = blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i :=
kroneckerMap_diagonal_right _ (tmul_zero _) _ _