mathlib
455f0603 - chore(unicode): improve arrows (#1373)

Commit

6 years ago

chore(unicode): improve arrows (#1373) * chore(unicode): improve arrows * grammar Co-Authored-By: Johan Commelin <johan@commelin.net> * moar

References

Author

khoek

Committer

mergify[bot]

Parents