-
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) : Add solution to IMO 1994 Q1 #10171
Conversation
archive/imo/imo1994_q1.lean
Outdated
rw this, clear this, | ||
|
||
-- The rest is a simple calculation by rearranging one of the two sums | ||
calc 2 * ∑ i : fin (m+1), a i = ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a i : two_mul _ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
calc 2 * ∑ i : fin (m+1), a i = ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a i : two_mul _ | |
calc 2 * ∑ i : fin (m+1), a i | |
= ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a i : two_mul _ |
Please reformat the other lines as well. Hopefully they'll fit in ≤ 100 chars that way.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, done!
@antoinelab01 I pushed some golfs and tricks to the branch |
Sorry, I'm still not very familiar with GitHub... I don't find this branch, where can I see it? |
You can see the diff here: imo1994_q1...imo1994_q1_jmc |
Thanks. How do I merge the golf you did to my pull request? |
@antoinelab01 Are you familiar with the command line? In your copy of mathlib, make sure you have checked out your branch: git checkout imo1994_q1
git fetch # pull updates from github
git merge origin/imo1994_q1_jmc # merge the other branch into yours |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
IMO 1994 Q1 Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
IMO 1994 Q1 Co-authored-by: Johan Commelin <johan@commelin.net>
IMO 1994 Q1