toDirectSum_intCast — Mathlib

English

Integer casts into AddMonoidAlgebra correspond to the same scalar in DirectSum when viewed via DirectSum.

Русский

Целочисленные приведения внутри AddMonoidAlgebra соответствуют тем же скалярам в DirectSum через отображение DirectSum.

LaTeX

$$$(\\text{Int.cast } z : AddMonoidAlgebra M ι).toDirectSum = z$$

Lean4

@[simp]
theorem toDirectSum_intCast [DecidableEq ι] [AddMonoid ι] [Ring M] (z : ℤ) :
    (Int.cast z : AddMonoidAlgebra M ι).toDirectSum = z :=
  Finsupp.toDFinsupp_single _ _

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