chore: assorted lake touchups

Open tydeu opened this issue 2 years ago • 1 comments

Oct 17 '23 21:10 tydeu

✅ Mathlib branch lean-pr-testing-2706 has successfully built against this PR. (2023-10-18 00:04:58) View Log

Oct 18 '23 00:10 leanprover-community-mathlib4-bot

Closing due to staleness and the fact that these changes have since been incorporated in other PRs.

Apr 10 '25 18:04 tydeu