toAlternatingMap_add — Mathlib

English

The operation toAlternatingMap is additive: (f+g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap.

Русский

Применение toAlternatingMap сохраняет сложение: (f+g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap.

LaTeX

$$$ (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap $$$

Lean4

@[simp]
theorem toAlternatingMap_add (f g : M [⋀^ι]→L[R] N) :
    (f + g).toAlternatingMap = f.toAlternatingMap + g.toAlternatingMap :=
  rfl

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