[Merged by Bors] - feat(archive/imo): formalize IMO 1969 problem 1 #4261
Conversation
bryangingechen
changed the title
bryangingechen
added
the
awaiting-author
|
@lacker I've sent you an invite to create branches in this repo. The advantage of opening PRs from branches in the main mathlib repo is that our CI scripts will generate olean files for each commit and upload them to our Azure server where they can be fetched by |
|
Thanks reviewers. I've responded to all items of feedback, please take another look! |
FYI, please change the label from |
jcommelin
added
awaiting-review
robertylewis
added
awaiting-author
lacker
added
awaiting-review
| lemma int_large (a : ℤ) (h : 1 < a) : 1 < a.nat_abs := | ||
| by exact_mod_cast lt_of_lt_of_le h le_nat_abs | ||
|
|
||
| lemma int_not_prime (a b : ℤ) (c : ℕ) (h1 : 1 < a) (h2 : 1 < b) (h3 : a*b = ↑c) : ¬ prime c := |
There was a problem hiding this comment.
| lemma int_not_prime (a b : ℤ) (c : ℕ) (h1 : 1 < a) (h2 : 1 < b) (h3 : a*b = ↑c) : ¬ prime c := | |
| lemma int_not_prime (a b : ℤ) (c : ℕ) (h₁ : 1 < a) (h₂ : 1 < b) (h₃ : a*b = ↑c) : ¬ prime c := |
Just a minor stylistic suggestion, not necessary to adopt. We love our unicode in mathlib. :-) You can type these just as \1, etc.
|
Looks great, thank you! bors d+ |
|
✌️ lacker can now approve this pull request. To approve and merge a pull request, simply reply with |
kim-em
added
delegated
|
bors r+ |
This is a formalization of the problem and solution for the first problem on the 1969 IMO: Prove that there are infinitely many natural numbers $a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This is a formalization of the problem and solution for the first problem on the 1969 IMO: Prove that there are infinitely many natural numbers $a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$
This is a formalization of the problem and solution for the first problem on the 1969 IMO:
Prove that there are infinitely many natural numbers$a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$
This is my first submission to mathlib, so please let me know if there are stylistic problems with this, or especially if I'm missing some easier way to do things.