Theorem CategoryTheory.GradedObject.hasTensor_of_iso

Modification history

2024-11-20 13:18
Mathlib/CategoryTheory/GradedObject/Monoidal.lean
feat: the monoidal category structure on homological complexes (#15695) …
Added CategoryTheory.GradedObject.hasTensor_of_isoView on Github →