Commit 2026-02-11 08:51 cdb0b33d

View on Github →

feat(Algebra/Homology): quasi-isomorphisms in functor categories (#35119)

Estimated changes

Modified Mathlib/Algebra/Homology/Functor.lean

added theorem CategoryTheory.ShortComplex.quasiIso_iff_evaluation

modified def HomologicalComplex.asFunctor

modified def HomologicalComplex.complexOfFunctorsToFunctorToComplex

added theorem HomologicalComplex.quasiIsoAt_iff_evaluation

added theorem HomologicalComplex.quasiIso_iff_evaluation