-
Notifications
You must be signed in to change notification settings - Fork 299
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.
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
[Merged by Bors] - feat(archive/imo): revive @kbuzzard's imo2019_q1 #4377
Conversation
I'll try to golf the proof. |
What does "golf" mean in this context? |
ascii length |
I took the opportunity to add some |
It seems that the CI doesn't run on this branch. I'm running the build locally. |
@dselsam I've sent you an invitation to access non-master branches of this repo. If you make a PR from a branch in this repo, then CI will build |
I've also pushed to https://github.com/leanprover-community/mathlib/tree/imo2019_q1 to make CI build it. |
new proof is much nicer! |
bors try |
tryBuild failed: |
I moved lemmas to a separate PR. |
bors try |
tryBuild succeeded: |
Thanks! |
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Yury Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This PR was included in a batch that was canceled, it will be automatically retried |
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Yury Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Kevin Buzzard k.buzzard@imperial.ac.uk
Co-authored-by: Yury Kudryashov urkud@urkud.name
Original version: https://gist.github.com/kbuzzard/b337639d471a135108511f4fab850e8b
simp
lemmas for IMO 2019 q1 #4383 supporting lemmas