toAddMonoidAlgebra_add — Mathlib

English

DirectSum respects addition: the DirectSum of f + g equals the sum of DirectSum of f and DirectSum of g.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toAddMonoidAlgebra_add [Semiring M] [∀ m : M, Decidable (m ≠ 0)] (f g : ⨁ _ : ι, M) :
    (f + g).toAddMonoidAlgebra = toAddMonoidAlgebra f + toAddMonoidAlgebra g :=
  DFinsupp.toFinsupp_add _ _

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