quadratic reciprocity

Stream: maths

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

What are good mathlib files to look at?

[Kevin Buzzard]

Oh I have it in Xena in M1F ;-)

[Kevin Buzzard]

That's handy :-)

[Kevin Buzzard]

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]

There is data.int.modeq now, too

[Kevin Buzzard]

Oh perfect! Many thanks.

[Chris Hughes]

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]

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]

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

[Kenny Lau]

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]

Sure it does, (n) is an ideal

[Kenny Lau]

but not a special one

[Kenny Lau]

n is as special as other elements in the ring

[Mario Carneiro]

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]

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

[Kenny Lau]

indeed

[Chris Hughes]

Why not PR it?

[Kenny Lau]

reasons

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

and then convert back to a ring

[Kenny Lau]

right

[Mario Carneiro]

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

[Kenny Lau]

so are you saying I should build the interface?

[Mario Carneiro]

right

[Mario Carneiro]

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

[Kenny Lau]

:)

[Kevin Buzzard]

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]

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