case h
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
a✝ : ℕ
⊢ ↑(toFinsupp []) a✝ = ↑0 a✝
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
⊢ toFinsupp [] = 0
ext
no goals
case h
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
a✝ : ℕ
⊢ ↑(toFinsupp []) a✝ = ↑0 a✝
simp