Mathlib v3 is deprecated. Go to Mathlib v4

Def list.sum

Modification history

2019-09-08 08:47
src/data/list/defs.lean
feat(data/list/defs): move list.sum to list/defs.lean (#1415) …
Added list.sumView on Github →
2017-11-10 05:26
data/list/basic.lean
refactor(algebra/group): Use a user attr for to_additive …
Deleted list.sumView on Github →
2017-10-15 01:58
data/list/basic.lean
feat(*): working on list/basic, robusting simp proofs
Modified list.sumView on Github →
2017-07-25 13:51
data/list/basic.lean
refactor(*): move in list lemmas, adapt to change in list.union
Added list.sumView on Github →