Zulip Chat Archive

Stream: maths

Topic: When is -2 a square mod p?


view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:58):

Is there a proof in Lean that if p is a prime congruent to 5 or 7 mod 8 then -2 is not a square mod p?

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:58):

This result drops out rather nicely from the Gauss' lemma approach

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:58):

One counts the number of multiples of -2, mod p, which are negative

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:59):

and it's rather easy to do

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:59):

That's the simplest proof I know.

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 22:59):

I don't know of an elementary trick (in contrast to -1 and -3 which can be done by hand using roots of unity)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:00):

https://en.wikipedia.org/wiki/Gauss%27s_lemma_(number_theory)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:00):

Uses Euler's criterion

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:01):

which uses that the Sylow 2-subgroup of (Z/pZ)(Z/pZ)^* is cyclic

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:01):

which follows from x^2-1=(x+1)(x-1)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:02):

Assuming Gauss' lemma, then you look at the sequence 2,4,6,...(p1)-2,-4,-6,...-(p-1)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:03):

and mod p this set is the same as 1,3,5,...,p-2 (reverse the order)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:03):

and Gauss' Lemma says that the number of elements of this sequence which are >p/2>p/2

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 23:04):

is odd if -2 is a non-square and even otherwise

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:48):

2018-04-28.png

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:48):

From the lecture notes of number theory (M345P14)

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:48):

@Kevin Buzzard

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:49):

That's 2

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:49):

we need -2

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:49):

oh well

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:49):

the symbol is multiplicative :P

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:50):

proof by euler criterion, I hope

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:50):

that's slightly deeper than you want

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:50):

yes

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:50):

which is elementary enough?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:50):

You can generalise the link you sent me to deal with the -2 case

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:50):

I see

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:50):

and in fact the -2 case comes out slightly nicer than the +2 case

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:51):

so we consider (-2)^q q! instead?

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:52):

and then after rearranging it turns out to be q!?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:57):

I can't guess what you mean

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:57):

There's something called Gauss' Lemma

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:57):

and it follows from that

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:57):

I think we should prove quadratic reciprocity :P

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:58):

that would be call

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:58):

cool

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 03:58):

See if Mario already did it

view this post on Zulip Kenny Lau (Apr 28 2018 at 03:58):

I don't think it's done

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:00):

I reckon I'll need 1000 lines to do it lol

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:00):

Do it after exams and write your M1R project on it

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:00):

heh...

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:01):

are you sure I should use QR as project... seems quite well known

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:19):

It would not be the first time that a 1st year undergraduate had done a project on something which some of the professors think is "quite well-known".

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:19):

On the other hand if you want to be top

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:19):

then you have to do something hard and do it well

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:19):

You could do affine schemes

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 04:19):

That would be impressive

view this post on Zulip Kenny Lau (Apr 28 2018 at 04:19):

lol


Last updated: May 10 2021 at 06:13 UTC