diagonal_kronecker — Mathlib

English

Kronecker product with a diagonal on the left yields a reindexed block-diagonal form.

Русский

Кронекерово произведение слева диагонали с A даёт повторное индексирование блочной диагонали.

LaTeX

$$diagonal a ⊗ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal (λ i. a i • B))$$

Lean4

theorem diagonal_kronecker [MulZeroClass α] [DecidableEq l] (a : l → α) (B : Matrix m n α) :
    diagonal a ⊗ₖ B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => a i • B) :=
  kroneckerMap_diagonal_left _ zero_mul _ _

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