zero_compAlternatingMap

Mathlib.LinearAlgebra.Alternating.Basic

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

English

Composing with the zero linear map yields the zero alternating map.

Русский

Композиция с нулевым линейным отображением даёт нулевое чередующее отображение.

LaTeX

$$$ (f) \circ_{\mathrm{Alt}} 0 = 0 $$$

Lean4

@[simp]
theorem zero_compAlternatingMap (f : M [⋀^ι]→ₗ[R] N) : (0 : N →ₗ[R] N₂).compAlternatingMap f = 0 :=
  rfl

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

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

Разделы

Аффилиация

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