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 #

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
@[simp]
theorem finsupp.to_alist_entries {α : Type u_1} {M : Type u_2} [has_zero M] (f : α →₀ M) :
@[simp]
theorem finsupp.to_alist_keys_to_finset {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] (f : α →₀ M) :
@[simp]
theorem finsupp.mem_to_alist {α : Type u_1} {M : Type u_2} [has_zero M] {f : α →₀ M} {x : α} :
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
@[simp]
theorem alist.lookup_finsupp_apply {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] (l : alist (λ (x : α), M)) (a : α) :
@[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
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) :
theorem alist.lookup_finsupp_eq_zero_iff {α : Type u_1} {M : Type u_2} [has_zero M] [decidable_eq α] {l : alist (λ (x : α), M)} {a : α} :
@[simp]
theorem alist.empty_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] :
@[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) :
@[simp]
theorem alist.singleton_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] (a : α) (m : M) :
@[simp]
theorem finsupp.to_alist_lookup_finsupp {α : Type u_1} {M : Type u_2} [has_zero M] (f : α →₀ M) :