Theorem HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁

Modification history

2024-03-24 11:48
Mathlib/Algebra/Homology/BifunctorHomotopy.lean
feat(Algebra/Homology): the action of a bifunctor on homological complexes factors through homotopies (#10800) …
Added HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁View on Github →