compAlternatingMap_add — Mathlib

English

The sum of two linear maps composed with an alternating map equals the sum of the compositions.

Русский

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

LaTeX

$$$ (g_1 + g_2) \cdot_{\mathrm{Alt}} f = g_1 \cdot_{\mathrm{Alt}} f + g_2 \cdot_{\mathrm{Alt}} f $$$

Lean4

@[simp]
theorem compAlternatingMap_add (g : N →ₗ[R] N₂) (f₁ f₂ : M [⋀^ι]→ₗ[R] N) :
    g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂ :=
  AlternatingMap.ext fun _ => map_add g _ _

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