Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Month in Mathlib May 2024 - Fixes (#78)
Indentation was wrong, some links were dead and a PR shouldn't have been mentioned.
- Loading branch information