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: small_iUnion and small_sUnion #10921

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat: small_iUnion and small_sUnion #10921

Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
8ec5f96
Add code
TwoFX Feb 24, 2024
93c33bb
Add to Mathlib.lean
TwoFX Feb 24, 2024
27076b5
Merge remote-tracking branch 'origin/master' into small-union
TwoFX Feb 25, 2024
d03fe16
Code review suggestions, switch to instance
TwoFX Feb 25, 2024
50a5ec7
Move
TwoFX Feb 25, 2024
7ec9649
Oops
TwoFX Feb 25, 2024
650e03f
Move back
TwoFX Feb 25, 2024
520f802
Move more
TwoFX Feb 25, 2024
0d3a865
Argh
TwoFX Feb 25, 2024
357a5aa
Fix SetTheory.Cardinal.Basic
TwoFX Feb 25, 2024
168f7ce
Fix CategoryTheory.Comma.StructuredArrow
TwoFX Feb 25, 2024
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
Prev Previous commit
Fix CategoryTheory.Comma.StructuredArrow
  • Loading branch information
@TwoFX
TwoFX committed Feb 25, 2024
commit 168f7ce6cb6605bf50dc7973b72cc6b5ca2919d6
1 change: 1 addition & 0 deletions Mathlib/CategoryTheory/Comma/StructuredArrow.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Comma.Basic
import Mathlib.CategoryTheory.PUnit
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
import Mathlib.CategoryTheory.EssentiallySmall
import Mathlib.Logic.Small.Set

#align_import category_theory.structured_arrow from "leanprover-community/mathlib"@"8a318021995877a44630c898d0b2bc376fceef3b"

Expand Down
Loading