Commit 2025-10-06 22:42 e3247322

View on Github →

feat(Data/List): relate destutter and dedup (#30228)

Estimated changes

Modified Mathlib/Data/List/Dedup.lean

added theorem List.dedup_cons'

added theorem List.dedup_cons

Modified Mathlib/Data/List/Destutter.lean

added theorem List.Pairwise.destutter_eq_dedup