mathlib
a63b99c3 - chore(category_theory/closed/monoidal): fix notation (#12612)

Commit
4 years ago
chore(category_theory/closed/monoidal): fix notation (#12612) Previously the `C` in the internal hom arrow ` ⟶[C] ` was hardcoded, which wasn't very useful! I've also reduced the precedence slightly, so we now require more parentheses, but I think these are less confusing rather than more so it is a good side effect? Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading