Zulip Chat Archive

Stream: maths

Topic: When is -2 a square mod p?

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?

Kevin Buzzard (Apr 27 2018 at 22:58):

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

Kevin Buzzard (Apr 27 2018 at 22:58):

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

Kevin Buzzard (Apr 27 2018 at 22:59):

and it's rather easy to do

Kevin Buzzard (Apr 27 2018 at 22:59):

That's the simplest proof I know.

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)

Kevin Buzzard (Apr 27 2018 at 23:00):

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

Kevin Buzzard (Apr 27 2018 at 23:00):

Uses Euler's criterion

Kevin Buzzard (Apr 27 2018 at 23:01):

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

Kevin Buzzard (Apr 27 2018 at 23:01):

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

Kevin Buzzard (Apr 27 2018 at 23:02):

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

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)

Kevin Buzzard (Apr 27 2018 at 23:03):

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

Kevin Buzzard (Apr 27 2018 at 23:04):

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

Kenny Lau (Apr 28 2018 at 03:48):

Kenny Lau (Apr 28 2018 at 03:48):

From the lecture notes of number theory (M345P14)

Kenny Lau (Apr 28 2018 at 03:48):

@Kevin Buzzard

Kevin Buzzard (Apr 28 2018 at 03:49):

That's 2

Kevin Buzzard (Apr 28 2018 at 03:49):

we need -2

Kenny Lau (Apr 28 2018 at 03:49):

oh well

Kenny Lau (Apr 28 2018 at 03:49):

the symbol is multiplicative :P

Kenny Lau (Apr 28 2018 at 03:50):

proof by euler criterion, I hope

Kevin Buzzard (Apr 28 2018 at 03:50):

that's slightly deeper than you want

Kevin Buzzard (Apr 28 2018 at 03:50):

yes

Kenny Lau (Apr 28 2018 at 03:50):

which is elementary enough?

Kevin Buzzard (Apr 28 2018 at 03:50):

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

Kenny Lau (Apr 28 2018 at 03:50):

I see

Kevin Buzzard (Apr 28 2018 at 03:50):

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

Kenny Lau (Apr 28 2018 at 03:51):

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

Kenny Lau (Apr 28 2018 at 03:52):

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

Kevin Buzzard (Apr 28 2018 at 03:57):

I can't guess what you mean

Kevin Buzzard (Apr 28 2018 at 03:57):

There's something called Gauss' Lemma

Kevin Buzzard (Apr 28 2018 at 03:57):

and it follows from that

Kenny Lau (Apr 28 2018 at 03:57):

I think we should prove quadratic reciprocity :P

Kevin Buzzard (Apr 28 2018 at 03:58):

that would be call

Kevin Buzzard (Apr 28 2018 at 03:58):

cool

Kevin Buzzard (Apr 28 2018 at 03:58):

See if Mario already did it

Kenny Lau (Apr 28 2018 at 03:58):

I don't think it's done

Kenny Lau (Apr 28 2018 at 04:00):

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

Kevin Buzzard (Apr 28 2018 at 04:00):

Do it after exams and write your M1R project on it

Kenny Lau (Apr 28 2018 at 04:00):

heh...

Kenny Lau (Apr 28 2018 at 04:01):

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

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".

Kevin Buzzard (Apr 28 2018 at 04:19):

On the other hand if you want to be top

Kevin Buzzard (Apr 28 2018 at 04:19):

then you have to do something hard and do it well

Kevin Buzzard (Apr 28 2018 at 04:19):

You could do affine schemes

Kevin Buzzard (Apr 28 2018 at 04:19):

That would be impressive

Kenny Lau (Apr 28 2018 at 04:19):

lol

Last updated: Dec 20 2023 at 11:08 UTC