Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-24 21:12 ee8451b9

View on Github →

feat(data/list): more lemmas on joins and sums (#2501) A few more lemmas on lists (especially joins) and sums. I also linted the file lists/basic.lean and converted some comments to section headers. Some lemmas got renamed: of_fn_prod_take -> prod_take_of_fn of_fn_sum_take -> sum_take_of_fn of_fn_prod ->prod_of_fn of_fn_sum -> sum_of_fn The arguments of nth_le_repeat were changed for better simp efficiency

Estimated changes

added theorem finset.univ_sigma_univ
deleted theorem list.of_fn_prod
deleted theorem list.of_fn_prod_take
deleted theorem list.of_fn_sum_take
added theorem list.prod_of_fn
added theorem list.prod_take_of_fn
added theorem list.sum_take_of_fn
added theorem prod_equiv
added theorem list.drop_append
added theorem list.drop_sum_join
added theorem list.eq_iff_join_eq
added theorem list.nth_le_drop'
added theorem list.nth_le_drop
added theorem list.nth_le_join
added theorem list.nth_le_of_eq
modified theorem list.nth_le_repeat
added theorem list.nth_le_take'
added theorem list.nth_le_take
added theorem list.take_append
added theorem list.take_repeat
added theorem list.take_sum_join
added theorem list.mem_of_fn