Skip to content

Commit 745e304

Browse files
committed
long file option for commsq.lean
1 parent 5e60c9f commit 745e304

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

  • Mathlib/CategoryTheory/Limits/Shapes/Pullback

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,6 @@ We define bicartesian squares, and
3939
show that the pullback and pushout squares for a biproduct are bicartesian.
4040
-/
4141

42-
4342
noncomputable section
4443

4544
open CategoryTheory
@@ -1533,3 +1532,5 @@ theorem IsPushout.map_iff {D : Type*} [Category D] (F : C ⥤ D) [PreservesColim
15331532
end Functor
15341533

15351534
end CategoryTheory
1535+
1536+
set_option linter.style.longFile 1700

0 commit comments

Comments
 (0)