finsuppLEquivDirectSum_symm_lof — Mathlib

English

Inverse maps lof back to singleton Finsupp: (finsuppLEquivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m.

Русский

Обратное отображение lof возвращает одиночный Finsupp.

LaTeX

$$$(finsuppLEquivDirectSum\, R\, M\, ι)^{\mathrm{symm}}(DirectSum.lof\, R\, ι\, (\lambda x, M)\, i\ m) = Finsupp.single\, i\ m$$$

Lean4

@[simp]
theorem finsuppLEquivDirectSum_symm_lof (i : ι) (m : M) :
    (finsuppLEquivDirectSum R M ι).symm (DirectSum.lof R ι _ i m) = Finsupp.single i m :=
  letI : ∀ m : M, Decidable (m ≠ 0) := Classical.decPred _
  DFinsupp.toFinsupp_single i m

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