Commit 2025-09-24 03:38 6317a928

View on Github →

chore: review of erw in Algebra/Homology/DerivedCategory (#23360)

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/Basic.lean

added theorem DerivedCategory.Qh_obj_singleFunctors_obj

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/SingleFunctors.lean

added theorem HomotopyCategory.quotient_obj_singleFunctors_obj

Modified Mathlib/CategoryTheory/Shift/SingleFunctors.lean