Commit 2025-03-21 20:58 c819e08a

View on Github →

feat(List): a list contains a single element iff it's a singleton (#20488) Adds setOf_eq_singleton_iff_of_nodup with the generalizing setOf_nodup_perm.

Estimated changes

Modified Mathlib/Data/List/Lemmas.lean

added theorem List.setOf_mem_eq_empty_iff

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.setOf_inj

added theorem Set.setOf_injective

Modified Mathlib/Data/Set/Insert.lean

added theorem Set.setOf_mem_list_eq_replicate

added theorem Set.setOf_mem_list_eq_singleton_of_nodup