toDirectSum_ofNat — Mathlib

English

If ι is a decidable finite set with an additive structure, the natural embedding of a nat n into AddMonoidAlgebra corresponds to the direct sum of n placed at a designated index.

Русский

При конечной декидной архитектуре ι и ADD моноидной структуре, естественное вложение числа n в AddMonoidAlgebra соответствует размещению n на одном индексе в DirectSum.

LaTeX

$$$(\\text{ofNat}(n) : AddMonoidAlgebra M ι).toDirectSum = \\text{ofNat}(n)$$$

Lean4

@[simp]
theorem toDirectSum_ofNat [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : AddMonoidAlgebra M ι).toDirectSum = ofNat(n) :=
  Finsupp.toDFinsupp_single _ _

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