Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-03 11:09 228ab96a

View on Github →

feat(data/list/destutter): add list.destutter to remove chained duplicates (#11934)

Estimated changes

Modified src/data/list/defs.lean

added def list.destutter'

added def list.destutter

Created src/data/list/destutter.lean

added theorem list.destutter'_cons

added theorem list.destutter'_cons_neg

added theorem list.destutter'_cons_pos

added theorem list.destutter'_eq_self_iff

added theorem list.destutter'_is_chain'

added theorem list.destutter'_is_chain

added theorem list.destutter'_ne_nil

added theorem list.destutter'_nil

added theorem list.destutter'_of_chain

added theorem list.destutter'_singleton

added theorem list.destutter'_sublist

added theorem list.destutter_cons'

added theorem list.destutter_cons_cons

added theorem list.destutter_eq_nil

added theorem list.destutter_eq_self_iff

added theorem list.destutter_idem

added theorem list.destutter_is_chain'

added theorem list.destutter_nil

added theorem list.destutter_of_chain'

added theorem list.destutter_pair

added theorem list.destutter_singleton

added theorem list.destutter_sublist

added theorem list.mem_destutter'