diagonal_kroneckerTMul — Mathlib

English

Kronecker product of two diagonals equals the diagonal of tensor products arranged by a product indexing isomorphism.

Русский

Кронекерово произведение двух диагоналей равно диагонали тензорных произведений, приведённой посредством диагонализации по индексации произведения.

LaTeX

$$diagonal a ⊗ₖₜ[R] diagonal b = diagonal (mn ↦ a m ⊗ₜ b n)$$

Lean4

theorem diagonal_kroneckerTMul [DecidableEq l] (a : l → α) (B : Matrix m n β) :
    diagonal a ⊗ₖₜ[R] B =
      Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b) :=
  kroneckerMap_diagonal_left _ (zero_tmul _) _
    _
      -- simp-normal form is `kroneckerTMul_assoc'`

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