mathlib

364d8714 - chore(data/list/big_operators): split (#17702)

chore(data/list/big_operators): split (#17702) Split `data.list.big_operators` into `.basic` and `.lemmas`, with the former containing no algebra or set imports. This should make more of the `fintype` dependency tree portable sooner.