Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-08 09:55 bd21cffc

View on Github →

feat(data/list/basic): some lemmas about sum/head/tail for list ℕ (#2342)

  • feat(data/list/basic): some lemmas about sum/head/tail for list ℕ
  • Add comment
  • remove lemma, moving to another PR
  • suggestion from review

Estimated changes

added theorem list.head_add_tail_sum
added theorem list.head_le_sum
added theorem list.tail_sum