Theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_inv_unit_unit

Modification history

2025-07-05 12:52
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
feat(CategoryTheory/Monoidal/DayConvolution): Associators and pentagon for Day Convolution (#25756) …
Added CategoryTheory.MonoidalCategory.DayConvolution.associator_inv_unit_unitView on Github →