Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-12 15:28 d9e96a3e

View on Github →

feat(data/list/dedup): Lemmas about list.dedup (#19142) Basic lemmas about dedup applied with cons, nil, head, and tail.

Estimated changes

Modified src/data/finset/basic.lean

added theorem list.to_finset_nonempty_iff

added theorem multiset.to_finset_nonempty

Modified src/data/list/dedup.lean

added theorem list.dedup_eq_cons

added theorem list.dedup_eq_nil

added theorem list.head_dedup

added theorem list.tail_dedup