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.

Estimated changes