finsuppLEquivDirectSum_single — Mathlib

English

The image of a singleton finsupp under finsuppLEquivDirectSum is the corresponding lof injection: finsuppLEquivDirectSum(...)(Finsupp.single i m) = DirectSum.lof ... i m.

Русский

Образ синглтона под эквивалентностью равен вложению lof: ...

LaTeX

$$$finsuppLEquivDirectSum\, R\, M\, ι\,(Finsupp.single\ i\ m) = DirectSum.lof\, R\, ι\, (\lambda k, M)\, i\ m$$$

Lean4

@[simp]
theorem finsuppLEquivDirectSum_single (i : ι) (m : M) :
    finsuppLEquivDirectSum R M ι (Finsupp.single i m) = DirectSum.lof R ι _ i m :=
  Finsupp.toDFinsupp_single i m

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