Commit 2023-01-11 04:58 c15ba021

View on Github →

feat: Port/data.list.destutter (#1466) feat: Port/Data.List.Destutter

Estimated changes

Modified Mathlib.lean

Created Mathlib/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'