[Merged by Bors] - feat(CategoryTheory/Monoidal): partially setting simp lemmas#10061
Closed
yuma-mizuno wants to merge 4 commits intomasterfrom ymizuno-whiskering-extracted4
+462-235
Commits
Commits on Jan 28, 2024
- committed
- committed
- committed
Commits on Jan 30, 2024
- committed