Theorems · Definition
AList.keys
{α : Type u} → {β : α → Type v} → AList β → List αThe list of keys of an association list.
- Defined in
- Mathlib.Data.List.AList
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AListstatement and proof · cited by 122
- List.keysproof · cited by 46
- AList.entriesproof · cited by 44
Cited by14
Results whose statement or proof uses this declaration.
- AList.mem_keysstatement · cited by 5
- AList.keys_replacestatement · cited by 2
- AList.Disjointproof · cited by 1
- AList.keys_erasestatement · cited by 1
- AList.keys_nodupstatement · cited by 1
- Finsupp.toAList_keys_toFinsetstatement · cited by 1
- AList.keys_emptystatement · cited by 0
- AList.keys_insertstatement · cited by 0
- AList.keys_mkstatement · cited by 0
- AList.keys_singletonstatement · cited by 0
- AList.keys_subset_keys_of_entries_subset_entriesstatement and proof · cited by 0
- Finmap.keys_extstatement · cited by 0