natCast_kronecker_natCast — Mathlib

English

Let a and b be natural numbers. The Kronecker product of the scalar matrices aI_m and bI_n is the diagonal matrix (ab)I_{mn}. In other words, (a I_m) ⊗ (b I_n) = (ab) I_{mn}.

Русский

Пусть a и b — натуральные числа. Кронеcker-продукт диагональных матриц aI_m и bI_n равен диагональной матрице (ab)I_{mn}. То есть (a I_m) ⊗ (b I_n) = (ab) I_{mn}.

LaTeX

$$$$(a I_m) \\otimes (b I_n) = (ab) I_{mn}$$$$

Lean4

@[simp]
theorem natCast_kronecker_natCast [NonAssocSemiring α] [DecidableEq m] [DecidableEq n] (a b : ℕ) :
    (a : Matrix m m α) ⊗ₖ (b : Matrix n n α) = ↑(a * b) :=
  (diagonal_kronecker_diagonal _ _).trans <| by simp_rw [← Nat.cast_mul]; rfl

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