Commit 2023-10-18 08:18 54436a74

View on Github →

chore(CategoryTheory.Triangulated): use more camelCase for distTriang (#7643) This PR renames lemmas like rot_of_dist_triang as rot_of_distTriang.

Estimated changes

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

added theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂

added theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃

added theorem CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁

deleted theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₁₂

deleted theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₂₃

deleted theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₃₁

added theorem CategoryTheory.Pretriangulated.inv_rot_of_distTriang

deleted theorem CategoryTheory.Pretriangulated.inv_rot_of_dist_triangle

added theorem CategoryTheory.Pretriangulated.rot_of_distTriang

deleted theorem CategoryTheory.Pretriangulated.rot_of_dist_triangle