Theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_naturality

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_naturalityView on Github →