toAddMonoidAlgebra_toDirectSum — Mathlib

English

The AddMonoidAlgebra corresponding to a DirectSum element recovers the original via the inverse direction, i.e., f.toAddMonoidAlgebra.toDirectSum = f.

Русский

Добавочная моноидальная алгебра через DirectSum восстанавливает исходное элемент через обратное направление.

LaTeX

$$$(f)^{\\text{toAddMonoidAlgebra}}^{\\text{toDirectSum}} = f$$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_toDirectSum (f : ⨁ _ : ι, M) : f.toAddMonoidAlgebra.toDirectSum = f :=
  (DFinsupp.toFinsupp_toDFinsupp (show Π₀ _ : ι, M from f) :)

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