Commit 2022-03-14 09:29 1f428f3e

View on Github →

feat(data/list/basic): Split and intercalate are inverses (#12466) Show that split and intercalate are inverses of each other (under suitable conditions)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.intercalate_split_on

added theorem list.modify_head_modify_head

added theorem list.split_on_intercalate

modified theorem list.split_on_p_aux_eq

added theorem list.split_on_p_aux_ne_nil

modified theorem list.split_on_p_aux_nil

added theorem list.split_on_p_aux_spec

added theorem list.split_on_p_cons

added theorem list.split_on_p_eq_single

added theorem list.split_on_p_first

added theorem list.split_on_p_ne_nil

added theorem list.split_on_p_nil

modified theorem list.split_on_p_spec