# Connections between Finsupp and AList#

## Main definitions #

• Finsupp.toAList
• AList.lookupFinsupp: converts an association list into a finitely supported function via AList.lookup, sending absent keys to zero.
@[simp]
theorem Finsupp.toAList_entries {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) :
f.toAList.entries = List.map Prod.toSigma f.graph.toList
noncomputable def Finsupp.toAList {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) :
AList fun (_x : α) => M

Produce an association list for the finsupp over its support using choice.

Equations
• f.toAList = { entries := List.map Prod.toSigma f.graph.toList, nodupKeys := }
Instances For
@[simp]
theorem Finsupp.toAList_keys_toFinset {α : Type u_1} {M : Type u_2} [Zero M] [] (f : α →₀ M) :
f.toAList.keys.toFinset = f.support
@[simp]
theorem Finsupp.mem_toAlist {α : Type u_1} {M : Type u_2} [Zero M] {f : α →₀ M} {x : α} :
x f.toAList f x 0
noncomputable def AList.lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] (l : AList fun (_x : α) => M) :
α →₀ M

Converts an association list into a finitely supported function via AList.lookup, sending absent keys to zero.

Equations
• l.lookupFinsupp = { support := (List.filter (fun (x : (_ : α) × M) => decide (x.snd 0)) l.entries).keys.toFinset, toFun := fun (a : α) => ().getD 0, mem_support_toFun := }
Instances For
@[simp]
theorem AList.lookupFinsupp_apply {α : Type u_1} {M : Type u_2} [Zero M] [] (l : AList fun (_x : α) => M) (a : α) :
l.lookupFinsupp a = ().getD 0
@[simp]
theorem AList.lookupFinsupp_support {α : Type u_1} {M : Type u_2} [Zero M] [] [] (l : AList fun (_x : α) => M) :
l.lookupFinsupp.support = (List.filter (fun (x : (_ : α) × M) => decide (x.snd 0)) l.entries).keys.toFinset
theorem AList.lookupFinsupp_eq_iff_of_ne_zero {α : Type u_1} {M : Type u_2} [Zero M] [] {l : AList fun (_x : α) => M} {a : α} {x : M} (hx : x 0) :
l.lookupFinsupp a = x x
theorem AList.lookupFinsupp_eq_zero_iff {α : Type u_1} {M : Type u_2} [Zero M] [] {l : AList fun (_x : α) => M} {a : α} :
l.lookupFinsupp a = 0 al 0
@[simp]
theorem AList.empty_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] :
.lookupFinsupp = 0
@[simp]
theorem AList.insert_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] [] (l : AList fun (_x : α) => M) (a : α) (m : M) :
(AList.insert a m l).lookupFinsupp = l.lookupFinsupp.update a m
@[simp]
theorem AList.singleton_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] (a : α) (m : M) :
().lookupFinsupp =
@[simp]
theorem Finsupp.toAList_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) :
f.toAList.lookupFinsupp = f
theorem AList.lookupFinsupp_surjective {α : Type u_1} {M : Type u_2} [Zero M] :
Function.Surjective AList.lookupFinsupp