diagonal_kroneckerTMul_diagonal — Mathlib

English

Kronecker product of two diagonal matrices is diagonal with entries given by pairwise tensor products of the diagonal entries.

Русский

Кронекерово произведение двух диагональных матриц снова диагональное, элементы которого — тензорные произведения соответствующих диагональных элементов.

LaTeX

$$kroneckerMap (diagonal a) (diagonal b) = diagonal (λ mn, a m ⊗ₜ b n)$$

Lean4

theorem diagonal_kroneckerTMul_diagonal [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → β) :
    diagonal a ⊗ₖₜ[R] diagonal b = diagonal fun mn => a mn.1 ⊗ₜ b mn.2 :=
  kroneckerMap_diagonal_diagonal _ (zero_tmul _) (tmul_zero _) _ _

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