kroneckerTMul_zero

Mathlib.LinearAlgebra.Matrix.Kronecker

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

English

The Kronecker product with a zero matrix on the right is the zero matrix.

Русский

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

LaTeX

$$A ⊗_R (0 : Matrix n p β) = 0$$

Lean4

theorem kroneckerTMul_zero (A : Matrix l m α) : A ⊗ₖₜ[R] (0 : Matrix n p β) = 0 :=
  kroneckerMap_zero_right _ (tmul_zero β) A

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

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

Разделы

Аффилиация

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