mathlib3 documentation

data.finsupp.alist

Connections between finsupp and alist #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

source
noncomputable def finsupp.to_alist {α : Type u_1} {M : Type u_2} [has_zero M] (f : α →₀ M) :
alist (λ (x : α), M)

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

Equations
source
@[simp]
theorem finsupp.to_alist_entries {α : Type u_1} {M : Type u_2} [has_zero M] (f : α →₀ M) :
f.to_alist.entries = list.map prod.to_sigma f.graph.to_list
source
@[simp]
theorem finsupp.to_alist_keys_to_finset {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] (f : α →₀ M) :
f.to_alist.keys.to_finset = f.support
source
@[simp]
theorem finsupp.mem_to_alist {α : Type u_1} {M : Type u_2} [has_zero M] {f : α →₀ M} {x : α} :
x ∈ f.to_alist ↔ ⇑f x ≠ 0
source
noncomputable def alist.lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] (l : alist (λ (x : α), M)) :
α →₀ M

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

Equations
source
@[simp]
theorem alist.lookup_finsupp_apply {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] (l : alist (λ (x : α), M)) (a : α) :
⇑(l.lookup_finsupp) a = (alist.lookup a l).get_or_else 0
source
@[simp]
theorem alist.lookup_finsupp_support {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] [decidable_eq M] (l : alist (λ (x : α), M)) :
l.lookup_finsupp.support = (list.filter (λ (x : Σ (x : α), M), x.snd ≠ 0) l.entries).keys.to_finset
source
theorem alist.lookup_finsupp_eq_iff_of_ne_zero {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] {l : alist (λ (x : α), M)} {a : α} {x : M} (hx : x ≠ 0) :
⇑(l.lookup_finsupp) a = x ↔ x ∈ alist.lookup a l
source
theorem alist.lookup_finsupp_eq_zero_iff {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] {l : alist (λ (x : α), M)} {a : α} :
⇑(l.lookup_finsupp) a = 0 ↔ a ∉ l ∨ 0 ∈ alist.lookup a l
source
@[simp]
theorem alist.empty_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] :
∅.lookup_finsupp = 0
source
@[simp]
theorem alist.insert_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] (l : alist (λ (x : α), M)) (a : α) (m : M) :
(alist.insert a m l).lookup_finsupp = l.lookup_finsupp.update a m
source
@[simp]
theorem alist.singleton_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] (a : α) (m : M) :
(alist.singleton a m).lookup_finsupp = finsupp.single a m
source
@[simp]
theorem finsupp.to_alist_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] (f : α →₀ M) :
f.to_alist.lookup_finsupp = f
source
theorem alist.lookup_finsupp_surjective {α : Type u_1} {M : Type u_2} [has_zero M] :
function.surjective alist.lookup_finsupp