Commit 2026-03-02 12:12 6588d0a2

View on Github →

feat(Algebra/Homology): limits of degreewise eventually constant projective systems (#35935)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/HomologicalComplexLimitsEventuallyConstant.lean

added theorem HomologicalComplex.isIso_π_f_of_isLimit_of_isEventuallyConstantTo

added theorem HomologicalComplex.quasiIsoAt_π_of_isLimit_of_isEventuallyConstantTo