Commit 2023-01-10 12:19 07eef429

View on Github →

feat: port Data.List.Join (#1395)

depends on: #1380

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Join.lean

added theorem List.append_join_map_append

added theorem List.bind_eq_nil

added theorem List.drop_sum_join

added theorem List.drop_take_succ_eq_cons_get

added theorem List.drop_take_succ_eq_cons_nthLe

added theorem List.drop_take_succ_join_eq_get

added theorem List.drop_take_succ_join_eq_nthLe

added theorem List.eq_iff_join_eq

added theorem List.join_append

added theorem List.join_concat

added theorem List.join_drop_length_sub_one

added theorem List.join_eq_nil

added theorem List.join_filter_isEmpty_eq_false

added theorem List.join_filter_ne_nil

added theorem List.join_join

added theorem List.join_reverse

added theorem List.join_singleton

added theorem List.length_bind

added theorem List.length_join

added theorem List.nthLe_join

added theorem List.reverse_join

added theorem List.sum_take_map_length_lt1

added theorem List.sum_take_map_length_lt2

added theorem List.take_sum_join

Modified Mathlib/Init/Align.lean