Commit 2022-11-23 18:12 eb620d2d
View on Github →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.
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.