Skip to content
Back to pull request #10898

[Merged by Bors] - feat(CategoryTheory/Monoidal): redefine tensorLeft by using whiskering #21029

Sign in to view logs

[Merged by Bors] - feat(CategoryTheory/Monoidal): redefine tensorLeft by using whiskering

[Merged by Bors] - feat(CategoryTheory/Monoidal): redefine tensorLeft by using whiskering #21029

Check all files imported

Check all files imported
succeeded Feb 29, 2024 in 9s