Def List.sum

Modification history

2023-12-10 22:40

Mathlib/Data/List/Defs.lean

chore: reduce imports of Data.List.Defs (#8635) …

Deleted List.sum View on Github →

2022-12-06 02:20

Mathlib/Data/List/Defs.lean

feat: port data.list.defs (#803) …

Added List.sum View on Github →