toDirectSum_sub — Mathlib

English

DirectSum is compatible with subtraction: the direct sum of f − g equals the difference of the direct sums.

Русский

DirectSum совместим с вычитанием: прямое сложение f − g эквивалентно разности их DirectSum-образов.

LaTeX

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

Lean4

@[simp]
theorem toDirectSum_sub [Ring M] (f g : AddMonoidAlgebra M ι) : (f - g).toDirectSum = f.toDirectSum - g.toDirectSum :=
  Finsupp.toDFinsupp_sub _ _

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