Commit 2024-07-16 09:12 63ed47e7

View on Github →

feat(CategoryTheory): the monoidal category structure on graded objects (#14457) Under suitable conditions on a monoidal category C, we define an instance of MonoidalCategory (GradedObject ℕ C). The construction is actually more general, and it shall be used in order to get monoidal category structures on homological complexes in future PRs.

Estimated changes