2025-08-28 18:47
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct` (#26798) …
Added CategoryTheory.MonoidalCategory.monoidalOfLawfulDayConvolutionMonoidalCategoryStruct