English
The image of a singleton element under the sigma-to-DFinsupp equivalence is exactly the corresponding singleton in the DFinsupp family.
Русский
Образ элемента-одиночки через эквивалентность между суммой и DFinsupp совпадает с соответствующим одиночным элементом в DFinsupp.
LaTeX
$$sigmaFinsuppEquivDFinsupp (Finsupp.single a n) = DFinsupp.single a.fst (Finsupp.single a.snd n)$$
Lean4
@[simp]
theorem sigmaFinsuppEquivDFinsupp_single [DecidableEq ι] [Zero N] (a : Σ i, η i) (n : N) :
sigmaFinsuppEquivDFinsupp (Finsupp.single a n) =
@DFinsupp.single _ (fun i => η i →₀ N) _ _ a.1 (Finsupp.single a.2 n) :=
by
obtain ⟨i, a⟩ := a
ext j b
by_cases h : i = j
· subst h
classical simp [split_apply, Finsupp.single_apply]
suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
classical
rw [Finsupp.single_apply, if_neg H]
-- Without this Lean fails to find the `AddZeroClass` instance on `Π₀ i, (η i →₀ N)`.
