Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-08 08:47 6f7224cc

View on Github →

feat(data/list/defs): move list.sum to list/defs.lean (#1415)

  • feat(data/list/defs): move list.sum to list/defs.lean
  • add comment

Estimated changes

added def list.sum