Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-10 15:57 d2b4380c

View on Github →

feat(data/list/basic): list.prod_range_succ, list.sum_range_succ (#1197)

  • feat(data/list/basic): list.prod_range_succ, list.sum_range_succ
  • changes from review
  • remove simp
  • shorten proof

Estimated changes