Zulip Chat Archive

Stream: maths

Topic: quadratic reciprocity


view this post on Zulip Kevin Buzzard (Apr 30 2018 at 23:34):

@Chris Hughes Did you prove Fermat's Little Theorem https://en.wikipedia.org/wiki/Fermat%27s_little_theorem in Lean? I am interested in proving Euler's Criterion https://en.wikipedia.org/wiki/Euler%27s_criterion and Gauss' Lemma https://en.wikipedia.org/wiki/Gauss%27s_lemma_(number_theory) in Lean, with a view to proving when -1 and +-2 are squares mod p (this is related to quadratic reciprocity).

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 23:34):

Is anything like that there already? Do we know the integers mod p are a field?

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 23:35):

What are good mathlib files to look at?

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 23:53):

Oh I have it in Xena in M1F ;-)

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 23:53):

That's handy :-)

view this post on Zulip Kevin Buzzard (May 01 2018 at 01:55):

Are the finite rings Z/nZ in Lean? I thought a bit about how to define them and decided that constructing the quotient of Z by the equivalence relation of being congruent mod n would be a really painless way to do it because all the lemmas would probably already be there. I found many of them all for nat in modeq but to avoid kerfuffle with neg I thought that Z would be better. How much of this stuff is already done?

view this post on Zulip Reid Barton (May 01 2018 at 02:21):

There is data.int.modeq now, too

view this post on Zulip Kevin Buzzard (May 01 2018 at 03:01):

Oh perfect! Many thanks.

view this post on Zulip Chris Hughes (May 01 2018 at 06:33):

I did get started on defining integers mod n. My effort is here. Some of the proofs are unfinished https://github.com/dorhinj/lean/blob/master/Zmod.lean

view this post on Zulip Chris Hughes (May 01 2018 at 06:35):

I thought it would probably be better to define this stuff in a general ring / euclidean domain, not just integers, especially after I ran into a load of trouble converting xgcd from nats into ints.

view this post on Zulip Johan Commelin (May 01 2018 at 07:13):

You mean that you want to define "ring mod ideal" in general? Or just "ring mod n"?

view this post on Zulip Kenny Lau (May 01 2018 at 07:18):

You mean that you want to define "ring mod ideal" in general? Or just "ring mod n"?

ring mod n doesn't make much sense in general, I think

view this post on Zulip Mario Carneiro (May 01 2018 at 07:18):

Sure it does, (n) is an ideal

view this post on Zulip Kenny Lau (May 01 2018 at 07:19):

but not a special one

view this post on Zulip Kenny Lau (May 01 2018 at 07:19):

n is as special as other elements in the ring

view this post on Zulip Mario Carneiro (May 01 2018 at 07:20):

I've been thinking about how to unify this idea with my idea for Z/nZ as fin n with better operations. I think the best option is just to keep the developments separate (ish), with a provable isomorphism Z/nZ -> Z mod (n) where (n) is the ideal generated by n

view this post on Zulip Chris Hughes (May 01 2018 at 07:20):

Didn't you do it in a general ring Kenny?

view this post on Zulip Kenny Lau (May 01 2018 at 07:20):

indeed

view this post on Zulip Chris Hughes (May 01 2018 at 07:21):

Why not PR it?

view this post on Zulip Kenny Lau (May 01 2018 at 07:21):

reasons

view this post on Zulip Mario Carneiro (May 01 2018 at 07:21):

For similar reasons to rat, I would not want Z/nZ to be a quotient when doing computations. This would make stuff like a^k : Z/nZ far too expensive

view this post on Zulip Kenny Lau (May 01 2018 at 07:21):

(it will just be an interface of linear_algebra.quotient_module and ring_theory.ideal)

view this post on Zulip Mario Carneiro (May 01 2018 at 07:23):

It's not completely trivial, you have to take a ring as a module over itself and then quotient by the ideal construed as a submodule

view this post on Zulip Mario Carneiro (May 01 2018 at 07:23):

and then convert back to a ring

view this post on Zulip Kenny Lau (May 01 2018 at 07:23):

right

view this post on Zulip Mario Carneiro (May 01 2018 at 07:23):

The theorems are probably easy specializations of existing theorems, but I think the specialization is worthwhile

view this post on Zulip Kenny Lau (May 01 2018 at 07:24):

so are you saying I should build the interface?

view this post on Zulip Mario Carneiro (May 01 2018 at 07:24):

right

view this post on Zulip Mario Carneiro (May 01 2018 at 07:24):

make it so users don't have to think about modules for ring theory

view this post on Zulip Kenny Lau (May 01 2018 at 07:24):

:)

view this post on Zulip Kevin Buzzard (May 01 2018 at 16:11):

n is as special as other elements in the ring

n is one of the elements you can guarantee is there in every ring, so it's special in some sense.

view this post on Zulip Kenny Lau (May 01 2018 at 16:11):

ah, you're on about the universal ring business again


Last updated: May 10 2021 at 07:15 UTC