Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Products #2564

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.Limits.Shapes.Products #2564

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
d482fe9
feat: port CategoryTheory.Limits.Shapes.Products
joelriou Mar 1, 2023
dd61b57
Initial file copy from mathport
joelriou Mar 1, 2023
b3b7993
automated fixes
joelriou Mar 1, 2023
407123b
started working on this file
joelriou Mar 1, 2023
0c322e1
removed most sorries
joelriou Mar 2, 2023
bcb153b
fixed sorries
joelriou Mar 2, 2023
4ffa8fc
Update Mathlib/CategoryTheory/Limits/Shapes/Products.lean
jcommelin Mar 2, 2023
294272f
Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits…
joelriou Mar 2, 2023
667aae4
Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits…
joelriou Mar 5, 2023
3f69416
Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits…
joelriou Mar 6, 2023
a82cc70
Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits…
joelriou Mar 7, 2023
4e61741
Merge remote-tracking branch 'origin' into port/CategoryTheory.Limits…
joelriou Mar 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -305,6 +305,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Limits.Shapes.Products
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Expand Down
Loading