toAddMonoidAlgebra_intCast — Mathlib

English

There is a natural equality identifying the integer z with its image in the direct sum representation, via the toAddMonoidAlgebra construction.

Русский

Существует естественное соответствие, идентифицирующее целое число z с его образом в представлении прямой суммы через построение toAddMonoidAlgebra.

LaTeX

$$$\bigl(z : \bigoplus_{i \in \iota} M\bigr) .\text{toAddMonoidAlgebra} = z$$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_intCast [AddMonoid ι] [Ring M] [∀ m : M, Decidable (m ≠ 0)] (z : ℤ) :
    (z : ⨁ _ : ι, M).toAddMonoidAlgebra = z :=
  DFinsupp.toFinsupp_single _ _

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