mathlib
8394e594 - feat(data/finset/basic): perm_of_nodup_nodup_to_finset_eq (#7588)

Commit
4 years ago
feat(data/finset/basic): perm_of_nodup_nodup_to_finset_eq (#7588) Also `finset.exists_list_nodup_eq`. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Author
Parents
Loading