mathlib
a0735864
- fix(*): fix padding around notations (#16333)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(*): fix padding around notations (#16333) I noticed a bunch of issues around padding in mathport, so I went through and fixed all the padding issues I could find in mathlib. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Author
digama0
Parents
4c0aa6e7
Loading