toAddMonoidAlgebra_natCast — Mathlib

English

The natural embedding of a natural number into a DirectSum representation via the DirectSum functor corresponds to itself.

Русский

Естественное вложение натурального числа в представление DirectSum через функтор DirectSum соответствует самому числу.

LaTeX

$$$(\\text{n} : \\bigoplus_{i} M).toDirectSum = \\text{n}$$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_natCast [AddMonoid ι] [Semiring M] [∀ m : M, Decidable (m ≠ 0)] (n : ℕ) :
    (n : ⨁ _ : ι, M).toAddMonoidAlgebra = n :=
  DFinsupp.toFinsupp_single _ _

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