Documentation

Mathlib.Data.Finsupp.AList

Connections between Finsupp and AList #

Main definitions #

source
@[simp]
theorem Finsupp.toAList_entries {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) :
(Finsupp.toAList f).entries = List.map Prod.toSigma (Finset.toList (Finsupp.graph f))
source
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
Instances For
    source
    @[simp]
    theorem Finsupp.toAList_keys_toFinset {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] (f : α →₀ M) :
    List.toFinset (AList.keys (Finsupp.toAList f)) = f.support
    source
    @[simp]
    theorem Finsupp.mem_toAlist {α : Type u_1} {M : Type u_2} [Zero M] {f : α →₀ M} {x : α} :
    x ∈ Finsupp.toAList f ↔ f x ≠ 0
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AList.lookupFinsupp_apply {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] (l : AList fun (_x : α) => M) (a : α) :
      (AList.lookupFinsupp l) a = Option.getD (AList.lookup a l) 0
      source
      @[simp]
      theorem AList.lookupFinsupp_support {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] [DecidableEq M] (l : AList fun (_x : α) => M) :
      (AList.lookupFinsupp l).support = List.toFinset (List.keys (List.filter (fun (x : (_ : α) × M) => decide (x.snd ≠ 0)) l.entries))
      source
      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) :
      (AList.lookupFinsupp l) a = x ↔ x ∈ AList.lookup a l
      source
      theorem AList.lookupFinsupp_eq_zero_iff {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] {l : AList fun (_x : α) => M} {a : α} :
      (AList.lookupFinsupp l) a = 0 ↔ a ∉ l ∨ 0 ∈ AList.lookup a l
      source
      @[simp]
      theorem AList.empty_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] :
      AList.lookupFinsupp ∅ = 0
      source
      @[simp]
      theorem AList.insert_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] [DecidableEq α] (l : AList fun (_x : α) => M) (a : α) (m : M) :
      AList.lookupFinsupp (AList.insert a m l) = Finsupp.update (AList.lookupFinsupp l) a m
      source
      @[simp]
      theorem AList.singleton_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] (a : α) (m : M) :
      AList.lookupFinsupp (AList.singleton a m) = Finsupp.single a m
      source
      @[simp]
      theorem Finsupp.toAList_lookupFinsupp {α : Type u_1} {M : Type u_2} [Zero M] (f : α →₀ M) :
      AList.lookupFinsupp (Finsupp.toAList f) = f
      source
      theorem AList.lookupFinsupp_surjective {α : Type u_1} {M : Type u_2} [Zero M] :
      Function.Surjective AList.lookupFinsupp