mathlib
86055c5d - split(data/{finset,set}/pointwise): Split off `algebra.pointwise` (#12831)

Commit
3 years ago
split(data/{finset,set}/pointwise): Split off `algebra.pointwise` (#12831) Split `algebra.pointwise` into * `data.set.pointwise`: Pointwise operations on `set` * `data.finset.pointwise`: Pointwise operations on `finset` I'm crediting * The same people for `data.set.pointwise` * Floris for #3541
Author
Parents
Loading