Theorem HomologicalComplex.leftUnitor'_inv_comm

Modification history

2024-11-20 13:18
Mathlib/Algebra/Homology/Monoidal.lean
feat: the monoidal category structure on homological complexes (#15695) …
Added HomologicalComplex.leftUnitor'_inv_commView on Github →