map_zero_right

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.map_zero_right

English

map f 0 = 0 for any f: M → P; right-zero law for tensor maps.

Русский

map f 0 = 0 для любого f: M → P; закон нуля справа.

LaTeX

$$$\\operatorname{map} f (0 : N \\to Q) = 0$$$

Lean4

@[simp]
theorem map_zero_right (f : M →ₗ[R] P) : map f (0 : N →ₗ[R] Q) = 0 :=
  (mapBilinear R M N P Q _).map_zero

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

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

Разделы

Аффилиация

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