toDirectSum_natCast — Mathlib

English

A natural number embedded into the AddMonoidAlgebra carries over to the DirectSum representation as the same scalar.

Русский

Число натурального типа, встроенное в AddMonoidAlgebra, сохраняет свой характер в представлении DirectSum как тот же скаляр.

LaTeX

$$$(n : \\mathbb{N}) \\text{ in } AddMonoidAlgebra M ι \\Rightarrow (n : \\bigoplus_{i} M) = n$$$

Lean4

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

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