Mathlib v3 is deprecated. Go to Mathlib v4

Theorem list.take_append_eq_append_take

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.take_append_eq_append_take View on Github →