natCast_kronecker — Mathlib

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]

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