zero_compMultilinearMap

Mathlib.LinearAlgebra.Multilinear.Basic

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

English

The left zero identity holds: (0 : M2 →ₗ[R] M3).compMultilinearMap f = 0.

Русский

Левая ноль-идентичность: (0 : M2 →ₗ[R] M3).compMultilinearMap f = 0.

LaTeX

$$$$ 0 \cdot \_ \; \mathrm{compMultilinearMap} f = 0 $$$$

Lean4

@[simp]
theorem zero_compMultilinearMap (f : MultilinearMap R M₁ M₂) : (0 : M₂ →ₗ[R] M₃).compMultilinearMap f = 0 :=
  rfl

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

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

Разделы

Аффилиация

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