erw [Finsupp.mapDomain_single]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.mapDomain (fun j => j) 1 = 1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
⊢ Finsupp.single 0 1 = 1