Mathlib Map

Theorems · Definition

AList.entries

{α : Type u} → {β : α → Type v} → AList β → List (Sigma β)

The underlying List of an AList

Defined in
Mathlib.Data.List.AList
Cited by
44 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AList.toFinmap · cited by 33AList.toFinmapAList.lookup · cited by 28AList.lookupAList.insert · cited by 27AList.insertAList.nodupKeys · cited by 15AList.nodupKeysAList.keys · cited by 13AList.keysAList.erase · cited by 12AList.eraseAList.ext · cited by 9AList.extAList.lookupFinsupp · cited by 9AList.lookupFinsuppAList.replace · cited by 4AList.replaceFinmap.liftOn_toFinmap · cited by 4Finmap.liftOn_toFinmapAList.lookup_insert · cited by 3AList.lookup_insertAList.mem_lookup_iff · cited by 3AList.mem_lookup_iffAList.entries_insert_of_notMem · cited by 2AList.entries_insert_of_n…AList.extract · cited by 2AList.extractAList.keys_replace · cited by 2AList.keys_replaceAList · cited by 122AListAList.entriesCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • AListstatement and proof · cited by 122

Cited by57

Results whose statement or proof uses this declaration.