prodMap_zero

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.prodMap_zero

English

The prodMap of zero maps is zero: (0 : M → M2).prodMap (0 : M2' → M4') = 0.

Русский

ProdMap нулевых отображений равен нулю: (0) prodMap (0) = 0.

LaTeX

$$$ (0 : M \\to M_2).prodMap (0 : M_3 \\to M_4) = 0 $$$

Lean4

@[simp]
theorem prodMap_zero : (0 : M →ₗ[R] M₂).prodMap (0 : M₃ →ₗ[R] M₄) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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