single_kronecker_single — Mathlib

English

The Kronecker product of two singleton matrices corresponds to the singleton product: single ia ja a ⊗ₖ single ib jb b = single ((ia, ib)) ((ja, jb)) (a b).

Русский

Кронекерово произведение двух единичных матриц даёт единичную матрицу размера пары индексов, со значением a·b.

LaTeX

$$$ \mathrm{single}_{ia,ja}(a) \otimes_k \mathrm{single}_{ib,jb}(b) = \mathrm{single}_{(ia,ib),(ja,jb)}(a b) $$$

Lean4

theorem single_kronecker_single [MulZeroClass α] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
    (ia : l) (ja : m) (ib : n) (jb : p) (a b : α) :
    single ia ja a ⊗ₖ single ib jb b = single (ia, ib) (ja, jb) (a * b) :=
  kroneckerMap_single_single _ _ _ _ _ zero_mul mul_zero _ _

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