kronecker_one — Mathlib

English

For any matrix A, A ⊗ I_n is a block-diagonal matrix whose diagonal blocks are copies of A (up to a permutation of indices).

Русский

Для любой матрицы A, A ⊗ I_n является блочно-диагональной матрицей, на диагонали которой стоят копии A (после перестановки индексов).

LaTeX

$$$$ A \\otimes I_n = \\operatorname{blockDiagonal}(\\lambda _ , A) $$$$

Lean4

theorem kronecker_one [MulZeroOneClass α] [DecidableEq n] (A : Matrix l m α) :
    A ⊗ₖ (1 : Matrix n n α) = blockDiagonal fun _ => A :=
  (kronecker_diagonal _ _).trans <| congr_arg _ <| funext fun _ => Matrix.ext fun _ _ => mul_one _

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