Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-08 07:20 cb8d8ace

View on Github →

feat (data/list/basic): lemmas about prod and take (#2345)

feat (data/list/basic): lemmas about prod and take
move lemma
one more
using to_additive properly

Estimated changes

Modified src/data/list/basic.lean

added theorem list.length_pos_of_prod_ne_one

added theorem list.length_pos_of_sum_ne_zero

added theorem list.length_pos_of_sum_pos

added theorem list.prod_take_mul_prod_drop

added theorem list.prod_take_succ

added theorem list.sum_take_add_sum_drop

added theorem list.sum_take_succ