Theorem HomologicalComplex.rightUnitor'_inv

Modification history

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