Theorem HomologicalComplex.tensor_unit_d₂

Modification history

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