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.