ofNat_kronecker — Mathlib

English

Let A be a matrix and b a Nat. Then A ⊗ₖ b.cast is reindexed to a blockDiagonal of b • A.

Русский

Пусть A — матрица, b — натуральное число. Тогда A ⊗ₖ b.cast эквивалентно перестановке индексов блока на B = b • A.

LaTeX

$$$ A \otimes_k b.cast = \operatorname{reindex} (\operatorname prodComm m l) (\operatorname prodComm n l) ( \operatorname{blockDiagonal} (\lambda x, (b) \cdot A ) ) $$$

Lean4

theorem ofNat_kronecker [NonAssocSemiring α] [DecidableEq l] (a : ℕ) [a.AtLeastTwo] (B : Matrix m n α) :
    (ofNat(a) : Matrix l l α) ⊗ₖ B =
      Matrix.reindex (.prodComm _ _) (.prodComm _ _) (blockDiagonal fun _ => (ofNat(a) : α) • B) :=
  diagonal_kronecker _ _

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