sigmaFinsuppEquivDFinsupp_add — Mathlib

English

The map sigmaFinsuppEquivDFinsupp preserves addition: applying it to f + g yields the sum of the images.

Русский

Преобразование sigmaFinsuppEquivDFinsupp сохраняет сложение: sigmaFinsuppEquivDFinsupp(f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g.

LaTeX

$$$\\text{sigmaFinsuppEquivDFinsupp}(f + g) = \\text{sigmaFinsuppEquivDFinsupp}(f) + \\text{sigmaFinsuppEquivDFinsupp}(g)$$$

Lean4

@[simp]
theorem sigmaFinsuppEquivDFinsupp_add [AddZeroClass N] (f g : (Σ i, η i) →₀ N) :
    sigmaFinsuppEquivDFinsupp (f + g) =
      (sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g : Π₀ i : ι, η i →₀ N) :=
  by
  ext
  rfl

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