mathlib
aa329229 - chore(data/set/pointwise): split file, reducing dependencies (#16950)

Commit
3 years ago
chore(data/set/pointwise): split file, reducing dependencies (#16950) This splits `data.set.pointwise` and `data.finset.pointwise` each into several smaller files. This allows us to remove or defer some imports, e.g. of `order.well_founded_set` and of `algebra.big_operators.basic`. No changes to statements of theorems, just relocating. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading