add_compAlternatingMap — Mathlib

English

The composition distributes over addition in the left linear map.

Русский

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

LaTeX

$$$ g \circ_{\mathrm{Alt}} (f_1 + f_2) = (g \circ_{\mathrm{Alt}} f_1) + (g \circ_{\mathrm{Alt}} f_2) $$$

Lean4

@[simp]
theorem add_compAlternatingMap (g₁ g₂ : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) :
    (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f :=
  rfl

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