...

dagurtomas · Jun 14, 2024 · 9d67b2e · 9d67b2e
1 parent 834ebd3
commit 9d67b2e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanCondensed/Projects/AB.lean b/LeanCondensed/Projects/AB.lean
@@ -32,7 +32,7 @@ example : I ⥤ ShortComplex A ≌ ShortComplex (I ⥤ A) :=
 
 lemma forall_exact_iff_functorEquivalence_exact (F : I ⥤ ShortComplex A) : (∀ i, (F.obj i).Exact) ↔
     ((functorEquivalence I A).inverse.obj F).Exact := by
-    sorry
+  sorry
 
 class HasExactLimitsOfShape : Prop where
   hasLimitsOfShape : HasLimitsOfShape I A := by infer_instance