mathlib3
32c8445a - split(data/list/*): split off `data.list.basic` (#10164)

Commit
4 years ago
split(data/list/*): split off `data.list.basic` (#10164) Killing the giants. This moves 700 lines off `data.list.basic` that were about * `list.sum` and `list.product` into `data.list.big_operators` * `list.countp` and `list.count` into `data.list.count` * `list.sigma` and `list.prod` into `data.list.sigma_prod`
Author
Parents
Loading