Commit 2023-07-16 09:12 15b639c9

View on Github →

chore: forward-port leanprover-community/mathlib#19142 (#5893)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem List.toFinset_nonempty_iff

added theorem Multiset.toFinset_nonempty

Modified Mathlib/Data/List/Dedup.lean

added theorem List.dedup_eq_cons

added theorem List.dedup_eq_nil

added theorem List.headI_dedup

added theorem List.tail_dedup