Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 15:49 7c0c16ca

View on Github →

feat(data/list/basic): Add lemmas about inits and tails (#4222)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.inits_append

added theorem list.inits_cons

added theorem list.inits_eq_tails

added theorem list.inits_reverse

added theorem list.map_reverse_inits

added theorem list.map_reverse_tails

added theorem list.reverse_involutive

added theorem list.tails_append

added theorem list.tails_cons

added theorem list.tails_eq_inits

added theorem list.tails_reverse

Modified src/data/list/zip.lean

added theorem list.mem_zip_inits_tails

Modified src/logic/function/basic.lean

added theorem function.involutive.comp_self