Theorem List.getElem_bijective_iff

Modification history

2025-11-24 11:02
Mathlib/Data/List/Nodup.lean
chore(Data/List): reduce imports (#31643) …
Modified List.getElem_bijective_iffView on Github →
2025-10-11 22:15
Mathlib/Data/List/Nodup.lean
feat(Data/List/Nodup): `get` is bijective iff `count = 1` (#30223)
Added List.getElem_bijective_iffView on Github →