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.

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 := ⋯ }

@[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

@[simp]

theorem Finsupp.toAList_keys_toFinset {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] (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 : α) => (AList.lookup a l).getD 0, mem_support_toFun := ⋯ }

@[simp]

theorem AList.lookupFinsupp_apply {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] (l : AList fun (_x : α) => M) (a : α) : l.lookupFinsupp a = (lookup a l).getD 0

@[simp]

theorem AList.lookupFinsupp_support {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] [DecidableEq 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] [DecidableEq α] {l : AList fun (_x : α) => M} {a : α} {x : M} (hx : x ≠ 0) : l.lookupFinsupp a = x ↔ x ∈ lookup a l

theorem AList.lookupFinsupp_eq_zero_iff {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] {l : AList fun (_x : α) => M} {a : α} : l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l

@[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] [DecidableEq α] (l : AList fun (_x : α) => M) (a : α) (m : M) : (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) : (singleton a m).lookupFinsupp = Finsupp.single a m

@[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 lookupFinsupp