one_kronecker_one — Mathlib

English

The Kronecker product of identity matrices equals the identity: I_m ⊗ I_n = I_{mn}.

Русский

Кронекерово произведение единичных матриц равно единице: I_m ⊗ I_n = I_{mn}.

LaTeX

$$$$ I_m \\otimes I_n = I_{mn} $$$$

Lean4

theorem one_kronecker_one [MulZeroOneClass α] [DecidableEq m] [DecidableEq n] :
    (1 : Matrix m m α) ⊗ₖ (1 : Matrix n n α) = 1 :=
  kroneckerMap_one_one _ zero_mul mul_zero (one_mul _)

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