kroneckerTMul_diagonal — Mathlib

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 _) _ _

Похожие утверждения