# Zulip Chat Archive

## Stream: maths

### Topic: quadratic reciprocity

#### 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).

#### Kevin Buzzard (Apr 30 2018 at 23:34):

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

#### Kevin Buzzard (Apr 30 2018 at 23:35):

What are good mathlib files to look at?

#### Kevin Buzzard (Apr 30 2018 at 23:53):

Oh I have it in Xena in M1F ;-)

#### Kevin Buzzard (Apr 30 2018 at 23:53):

That's handy :-)

#### 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?

#### Reid Barton (May 01 2018 at 02:21):

There is `data.int.modeq`

now, too

#### Kevin Buzzard (May 01 2018 at 03:01):

Oh perfect! Many thanks.

#### 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

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

#### 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"?

#### 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

#### Mario Carneiro (May 01 2018 at 07:18):

Sure it does, (n) is an ideal

#### Kenny Lau (May 01 2018 at 07:19):

but not a special one

#### Kenny Lau (May 01 2018 at 07:19):

n is as special as other elements in the ring

#### 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

#### Chris Hughes (May 01 2018 at 07:20):

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

#### Kenny Lau (May 01 2018 at 07:20):

indeed

#### Chris Hughes (May 01 2018 at 07:21):

Why not PR it?

#### Kenny Lau (May 01 2018 at 07:21):

reasons

#### 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

#### Kenny Lau (May 01 2018 at 07:21):

(it will just be an interface of `linear_algebra.quotient_module`

and `ring_theory.ideal`

)

#### 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

#### Mario Carneiro (May 01 2018 at 07:23):

and then convert back to a ring

#### Kenny Lau (May 01 2018 at 07:23):

right

#### Mario Carneiro (May 01 2018 at 07:23):

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

#### Kenny Lau (May 01 2018 at 07:24):

so are you saying I should build the interface?

#### Mario Carneiro (May 01 2018 at 07:24):

right

#### Mario Carneiro (May 01 2018 at 07:24):

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

#### Kenny Lau (May 01 2018 at 07:24):

:)

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

#### 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