basic): downgrade `data.nat.order` import (#17691)

Commit

3 years ago

chore(data/fin/basic): downgrade `data.nat.order` import (#17691) Import `data.nat.order.basic` instead of `data.nat.order.lemmas` in `data.fin.basic`.

Author

hrmacbeth

Parents

f340f229

mathlib eb620d2d - chore(data/fin/basic): downgrade `data.nat.order` import (#17691)

mathlib
eb620d2d - chore(data/fin/basic): downgrade `data.nat.order` import (#17691)