refactor(CategoryTheory/Monoidal): add whiskering operators#6307
Draft
yuma-mizuno wants to merge 79 commits intomasterfrom ymizuno-monoidal-whiskering
+325-280
Commits
Commits on Aug 2, 2023
- committed
- committed
- committed
Commits on Aug 3, 2023
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Aug 4, 2023
Commits on Aug 5, 2023
- committed
- committed
- committed
- committed
Commits on Aug 6, 2023
- committed
- committed
Commits on Aug 7, 2023
- committed
- committed
Merge branch 'ymizuno-monoidal-whiskering' of https://github.com/leanprover-community/mathlib4 into ymizuno-monoidal-whiskering
committed- committed
- committed
- committed
- committed
Commits on Sep 21, 2023
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Nov 4, 2023
Commits on Nov 5, 2023
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Nov 7, 2023
Commits on Nov 8, 2023
Commits on Jan 6, 2024
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Jan 24, 2024
Commits on Jan 25, 2024
Commits on Jan 27, 2024
Commits on Feb 3, 2024
Commits on Mar 2, 2024
Commits on Mar 4, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed