Theorems · Definition
List.NodupKeys
{α : Type u} → {β : α → Type v} → List (Sigma β) → PropDetermines whether the store uses a key several times.
- Defined in
- Mathlib.Data.List.Sigma
- Cited by
- 53 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.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- List.keysproof · cited by 46
Cited by62
Results whose statement or proof uses this declaration.
- AList.nodupKeysstatement · cited by 15
- Multiset.NodupKeysproof · cited by 12
- AList.extproof · cited by 9
- AList.insertRecproof · cited by 4
- List.mem_dlookup_iffstatement and proof · cited by 4
- Finmap.liftOn_toFinmapproof · cited by 4
- List.nodupKeys_consstatement · cited by 4
- List.nodupKeys_iff_pairwisestatement · cited by 4
- AList.casesOnstatement and proof · cited by 3
- List.NodupKeys.kerasestatement · cited by 3
- List.lookup_extstatement and proof · cited by 3
- List.nodupKeys_of_nodupKeys_consstatement and proof · cited by 3