[Merged by Bors] - feat(Algebra/Homology): the mapping cone

[joelriou]

This PR completes the basic API for the mapping cone which shall be used in order to show that the homotopy category of cochain complexes is a triangulated category.

---

• depends on: [Merged by Bors] - feat(Algebra/Homology): binary biproducts of homological complexes #8966
• depends on: [Merged by Bors] - feat(Algebra/Homology): construction of the homotopy cofiber #8969
• depends on: [Merged by Bors] - feat(Algebra/Homology): morphisms from the homotopy cofiber #9447
• depends on: [Merged by Bors] - feat(Algebra/Homology): the cylinder of a homological complex #9483
• depends on: [Merged by Bors] - feat(Algebra/Homology): definition of the mapping cone #9508
• depends on: [Merged by Bors] - feat(Algebra/Homology): morphisms from the mapping cone #9509

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Algebra/Homology): binary biproducts of homological complexes #8966
• [Merged by Bors] - feat(Algebra/Homology): construction of the homotopy cofiber #8969
• [Merged by Bors] - feat(Algebra/Homology): morphisms from the homotopy cofiber #9447
• [Merged by Bors] - feat(Algebra/Homology): the cylinder of a homological complex #9483
• [Merged by Bors] - feat(Algebra/Homology): definition of the mapping cone #9508
• [Merged by Bors] - feat(Algebra/Homology): morphisms from the mapping cone #9509
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Lint style

[mathlib-bors]

Build failed:

• Build

[joelriou]

Retrying...

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style