Def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnit

Modification history

2025-12-16 19:53
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
chore(CategoryTheory): fix whitespace (#32928)
Modified CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnitView on Github →
2025-08-28 18:47
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct` (#26798) …
Added CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnitView on Github →