English
Let ι be an additive monoid and M a semiring. For any natural number n with n ≥ 2, the element of the direct sum ⨁_{ι} M corresponding to n concentrated at a single index, when mapped into AddMonoidAlgebra, is equal to the canonical embedding of n in AddMonoidAlgebra.
Русский
Пусть ι — моноид сложения, а M — полукольцо. Для любого натурального числа n, удовлетворяющего условию n ≥ 2, образ элемента DirectSum, представляющий n в виде единичной подпосылки в прямой сумме, в AddMonoidAlgebra совпадает с каноническим вложением n в AddMonoidAlgebra.
LaTeX
$$$ (\operatorname{ofNat}(n) : \bigoplus_{i:\,\iota} M).toAddMonoidAlgebra = \operatorname{ofNat}(n) $$$
Lean4
@[simp]
theorem toAddMonoidAlgebra_ofNat [AddMonoid ι] [Semiring M] [∀ m : M, Decidable (m ≠ 0)] (n : ℕ) [n.AtLeastTwo] :
(ofNat(n) : ⨁ _ : ι, M).toAddMonoidAlgebra = ofNat(n) :=
DFinsupp.toFinsupp_single _ _
