mathlib3
26a3e31d - chore(category_theory/monoidal): monoidal_category doesn't extend category (#1338)

Commit
6 years ago
chore(category_theory/monoidal): monoidal_category doesn't extend category (#1338) * chore(category_theory/monoidal): monoidal_category doesn't extend category * remove _aux file, simplifying * make notations global, and add doc-strings
Author
Committer
Parents
Loading