Theorem DerivedCategory.quotientCompQhIso_inv_naturality

Modification history

2026-05-06 01:11
Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
feat(Algebra/Homology): quasi-isomorphisms between chain complexes of projective objects are homotopy equivalences (#38958) …
Added DerivedCategory.quotientCompQhIso_inv_naturalityView on Github →