Skip to content

Commit 0a791e3

Browse files
committed
chore(CategoryTheory/Limits): move FormalCoproducts to new folder (leanprover-community#35016)
1 parent 43178d5 commit 0a791e3

3 files changed

Lines changed: 408 additions & 402 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2635,6 +2635,7 @@ public import Mathlib.CategoryTheory.Limits.Final.Type
26352635
public import Mathlib.CategoryTheory.Limits.FinallySmall
26362636
public import Mathlib.CategoryTheory.Limits.FintypeCat
26372637
public import Mathlib.CategoryTheory.Limits.FormalCoproducts
2638+
public import Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
26382639
public import Mathlib.CategoryTheory.Limits.Fubini
26392640
public import Mathlib.CategoryTheory.Limits.FullSubcategory
26402641
public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

0 commit comments

Comments
 (0)