Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-14 08:56 0f06bccf

View on Github →

feat(data/list/{basic,join}): towards take_join (#17190)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.drop_length_cons

added theorem list.nth_le_length_sub_one

added theorem list.take_add

added theorem list.take_eq_take

added theorem list.take_one_drop_eq_of_lt_length

Modified src/data/list/join.lean

added theorem list.join_drop_length_sub_one

deleted theorem list.join_nil

added theorem list.join_singleton