add doc string

leanprover-community · Dec 28, 2024 · ab4d5ee · ab4d5ee
1 parent 6372b3a
commit ab4d5ee
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/CategoryTheory/Triangulated/Adjunction.lean b/Mathlib/CategoryTheory/Triangulated/Adjunction.lean
@@ -34,6 +34,9 @@ variable {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommSh
   [adj.CommShift ℤ] [F.IsTriangulated]
 
 include adj in
+/--
+The right adjoint of a triangulated functor is triangulated.
+-/
 lemma isTriangulated_rightAdjoint : G.IsTriangulated where
   map_distinguished T hT := by
     have : G.Additive := adj.right_adjoint_additive