Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 07:19 f5ee47b6

View on Github →

feat(category_theory/triangulated): upgrade map_triangle to a functor (#13262) Useful for LTE.

Estimated changes

Modified src/category_theory/triangulated/pretriangulated.lean

modified def category_theory.triangulated.pretriangulated.triangulated_functor.map_triangle

added def category_theory.triangulated.pretriangulated.triangulated_functor_struct.id

modified def category_theory.triangulated.pretriangulated.triangulated_functor_struct.map_triangle

Modified src/category_theory/triangulated/rotate.lean

modified def category_theory.triangulated.from_inv_rotate_rotate

modified def category_theory.triangulated.from_rotate_inv_rotate

modified def category_theory.triangulated.inv_rot_comp_rot

modified def category_theory.triangulated.inv_rot_comp_rot_hom

modified def category_theory.triangulated.inv_rot_comp_rot_inv

modified def category_theory.triangulated.inv_rotate

modified def category_theory.triangulated.rot_comp_inv_rot

modified def category_theory.triangulated.rot_comp_inv_rot_hom

modified def category_theory.triangulated.rot_comp_inv_rot_inv

modified def category_theory.triangulated.rotate

modified def category_theory.triangulated.to_inv_rotate_rotate

modified def category_theory.triangulated.to_rotate_inv_rotate