mathlib3
chore(category_theory/binary_products): tweak spacing in notation
#2184
Merged
Merged
chore(category_theory/binary_products): tweak spacing in notation #2184
mergify
merged
3 commits into
master
from
binary_products_notation
chore(category_theory/binary_products): tweak spacing in notation
b1d2c88a
gebner
approved these changes
on 2020-03-18
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into binary_products_notation
c4554876
Merge branch 'master' into binary_products_notation
dad3ef7b
Login to write a write a comment.
Login via GitHub