Commit 2023-12-27 09:01 e0f4e431

View on Github →

feat(Algebra/Homology): construction of the homotopy cofiber (#8969)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Homotopy.lean

added theorem dNext_eq_zero

added theorem prevD_eq_zero

Created Mathlib/Algebra/Homology/HomotopyCofiber.lean

added theorem HomologicalComplex.homotopyCofiber.d_fstX

added theorem HomologicalComplex.homotopyCofiber.d_sndX

added theorem HomologicalComplex.homotopyCofiber.ext_from_X'

added theorem HomologicalComplex.homotopyCofiber.ext_from_X

added theorem HomologicalComplex.homotopyCofiber.ext_to_X'

added theorem HomologicalComplex.homotopyCofiber.ext_to_X

added theorem HomologicalComplex.homotopyCofiber.inlX_d'

added theorem HomologicalComplex.homotopyCofiber.inlX_d

added theorem HomologicalComplex.homotopyCofiber.inlX_fstX

added theorem HomologicalComplex.homotopyCofiber.inlX_sndX

added theorem HomologicalComplex.homotopyCofiber.inrX_d

added theorem HomologicalComplex.homotopyCofiber.inrX_fstX

added theorem HomologicalComplex.homotopyCofiber.inrX_sndX

added theorem HomologicalComplex.homotopyCofiber.shape

added theorem HomologicalComplex.homotopyCofiber.sndX_inrX