compAlternatingMap_zero — Mathlib

English

Composing an alternating map with two linear maps in succession is the same as composing with their linear composition.

Русский

Сочетание чередующегося отображения с двумя линейными отображениями подряд эквивалентно композиции с их линейной композицией.

LaTeX

$$$ (f \circ_{\mathrm{Alt}} g_1) \circ_{\mathrm{Alt}} g_2 = f \circ_{\mathrm{Alt}} (g_1 \circ g_2) $$$

Lean4

@[simp]
theorem compAlternatingMap_zero (g : N →ₗ[R] N₂) : g.compAlternatingMap (0 : M [⋀^ι]→ₗ[R] N) = 0 :=
  AlternatingMap.ext fun _ => map_zero g

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