nodup): Add `list.nodup_iff` (#14371)

Commit

3 years ago

feat(data/list/nodup): Add `list.nodup_iff` (#14371) Add `list.nodup_iff` and two helper lemmas `list.nth_le_eq_iff` and `list.some_nth_le_eq`

Author

user7230724

Parents