kronecker_natCast — Mathlib

English

For a matrix A and a natural b, the Kronecker product A ⊗ (b I_n) is a block-diagonal matrix with every block equal to b·A. Equivalently, A ⊗ₖ (b I_n) = blockDiagonal (λ → b·A).

Русский

Для матрицы A и натурального b кронеcker-продукт A ⊗ (b I_n) является блочно-диагональной матрицей, у которой каждый блок равен b·A. Это выражается как A ⊗ₖ (b I_n) = blockDiagonal (λ → b·A).

LaTeX

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

Lean4

theorem kronecker_natCast [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ℕ) :
    A ⊗ₖ (b : Matrix n n α) = blockDiagonal fun _ => b • A :=
  kronecker_diagonal _ _ |>.trans <| by
    congr! 2
    ext
    simp [(Nat.cast_commute b _).eq]

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