mathlib
ca2c3443 - split(data/finsupp/order): Split off `data.finsupp.basic` (#11045)

Commit
3 years ago
split(data/finsupp/order): Split off `data.finsupp.basic` (#11045) This moves all order instances about `finsupp` from `data.finsupp.basic` and `data.finsupp.lattice` to a new file `data.finsupp.order`. I'm crediting * Johan for #1216, #1244 * Aaron Anderson for #3335
Author
Parents
Loading