zero_kronecker

Mathlib.LinearAlgebra.Matrix.Kronecker

URI: https://scilib.ai/kg/mathlib#Matrix.zero_kronecker

English

If B is any matrix and A = 0, then A ⊗ₖ B = 0; similarly, B ⊗ₖ 0 = 0.

Русский

Если A = 0, то A ⊗ₖ B = 0; также B ⊗ₖ 0 = 0.

LaTeX

$$$ (0 : \mathrm{Matrix}_{l m}(\alpha)) \otimes_{k} B = 0$ и $A \otimes_{k} 0 = 0$$$

Lean4

theorem zero_kronecker [MulZeroClass α] (B : Matrix n p α) : (0 : Matrix l m α) ⊗ₖ B = 0 :=
  kroneckerMap_zero_left _ zero_mul B

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru