kronecker_zero

Mathlib.LinearAlgebra.Matrix.Kronecker

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

English

If one factor is zero, the Kronecker product is the zero matrix.

Русский

Если любая из матриц равна нулю, Кронекерово произведение равно нулевой матрице.

LaTeX

$$$A \otimes_{k} 0 = 0$ и $0 \otimes_{k} B = 0$$$

Lean4

theorem kronecker_zero [MulZeroClass α] (A : Matrix l m α) : A ⊗ₖ (0 : Matrix n p α) = 0 :=
  kroneckerMap_zero_right _ mul_zero A

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

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

Разделы

Аффилиация

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