Commit 2023-11-17 18:20 05ad6c6d

View on Github →

feat: add some Multiset.Nodup lemmas (#8464) Based on results from flt-regular.

Estimated changes

Modified Mathlib/Data/List/Nodup.lean

added theorem List.nodup_iff_count_eq_one

Modified Mathlib/Data/Multiset/Nodup.lean

added theorem Multiset.nodup_iff_count_eq_one

added theorem Multiset.nodup_map_iff_of_inj_on

added theorem Multiset.nodup_map_iff_of_injective