fix(Wikipedia/WallSunSun): assume the discriminant is 0 or 1 mod 4 #1528
Conversation
Co-authored-by: Calle Sönne <csonne@google.com>
YaelDillies
changed the title
infinite_isWallSunSunPrime_of_disc_eq
YaelDillies
changed the title
YaelDillies
added
awaiting-author
YaelDillies
removed
the
awaiting-author
| {p : ℕ | ∃ a b : ℕ, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p }.Infinite := by | ||
| theorem infinite_isWallSunSunPrime_of_disc_eq {D : ℕ} (hD₀ : 0 < D) | ||
| (hD : D ≡ 0 [MOD 4] ∨ D ≡ 1 [MOD 4]) : | ||
| {p : ℕ | ∃ a b : ℕ, a ^ 2 - 4 * b = D ∧ IsLucasWieferichPrime a b p}.Infinite := by |
There was a problem hiding this comment.
Should this be integer subtraction instead of nat subtraction?
There was a problem hiding this comment.
That doesn't change the mathematical content since D > 0
There was a problem hiding this comment.
Why do we have D>0 in the first place? I don't see it in the english.
There was a problem hiding this comment.
This is a mess. The Wikipedia conjecture is unsourced, and I cannot find back the source in an hour of searching... In the future we should enforce that conjectures are sourced
There was a problem hiding this comment.
My guess is that we added the condition ourselves to avoid this being incorrect when the subtraction truncates.
There was a problem hiding this comment.
No, this seems wrong. D is supposed to be the discriminant of a quadratic field, so it certainly cannot be a square
4 participants
No description provided.