Commit 2022-11-19 21:45 74921b80

View on Github →

chore(data/list/basic): streamline imports (#17616) From the imports of data.nat.order.basic: Remove data.set.basic, by moving four lemmas to data.nat.order.lemmas. From the imports of data.list.basic: Remove algebra.order.with_zero and data.set.function and downgrade data.nat.order.lemmas to data.nat.order.basic, by moving four lemmas to a new file data.list.lemmas and re-wording a couple of proofs.

Estimated changes