Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.drop_append_eq_append_drop

Modification history

2021-09-18 02:27

src/data/list/basic.lean

feat(data/list/basic): add lemmas about list.take list.drop (#9245) …

Added list.drop_append_eq_append_drop View on Github →