toDirectSum_add — Mathlib

English

DirectSum preserves addition: the direct sum of f + g corresponds to the sum of their direct sums.

Русский

DirectSum сохраняет сложение: прямое сумма f + g соответствует сумме их прямых сумм.

LaTeX

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

Lean4

@[simp]
theorem toDirectSum_add [Semiring M] (f g : AddMonoidAlgebra M ι) :
    (f + g).toDirectSum = f.toDirectSum + g.toDirectSum :=
  Finsupp.toDFinsupp_add _ _

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