## Stream: Is there code for X?

### Topic: Dirichlet's theorem on arithmetic progressions?

#### Manuel Candales (Apr 01 2021 at 21:46):

Is the Dirichlet's theorem on arithmetic progressions already implemented, or any of the special cases (like the infinitude of primes of the form 4k+1, 4k-1, etc)?
I didn't find this after doing a google site search or after looking through nat.prime and through the list of 100 theorems.

#### Kevin Buzzard (Apr 01 2021 at 21:47):

This is a nontrivial theorem; the standard proof involves a bunch of complex analysis and we have essentially no complex analysis. The special cases such as 4k+1, 4k-1 are easily accessible; we have enough about cyclotomic polynomials to do 1 mod N and indeed this might also be done.

#### Manuel Candales (Apr 01 2021 at 21:49):

I'll like to implement those, if you don't mind. How should I call them (still don't fully get the naming convention), and where should I place them? in nat.prime?

#### Bhavik Mehta (Apr 01 2021 at 21:51):

https://leanprover-community.github.io/mathlib_docs/number_theory/primes_congruent_one.html Here's the case for 1 mod N

#### Riccardo Brasca (Apr 01 2021 at 21:51):

As a special case we have docs#nat.exists_prime_ge_modeq_one for primes congruent to 1 mod N

ah, nice!

#### Kevin Buzzard (Apr 01 2021 at 22:23):

If you do 4k-1 you can also do 6k-1, this is the other elementary one. In general you can prove there's infinitely many primes not in a proper subgroup of $(\Z/N\Z)^\times$ by elementary methods but you only get a concrete equality when this group has order 2

#### Bhavik Mehta (Apr 02 2021 at 03:28):

There are a couple more special cases which should be doable without the heavy complex analysis, eg in https://kconrad.math.uconn.edu/blurbs/ugradnumthy/squaresandinfmanyprimes.pdf

#### Johan Commelin (Apr 02 2021 at 04:38):

Manuel Candales said:

How should I call them (still don't fully get the naming convention)?

Don't worry about that. Once you have a statement in Lean, you can post it here, and then more experienced users will be able to explain to you how to deduce the Lean name from the statement.

#### Kevin Buzzard (Apr 02 2021 at 08:18):

Yeah if you allow quadratic reciprocity (which we have in mathlib) then you can get a little further. There are very elementary methods (which don't use Z/pZ^* cyclic) for classifying when -1 and -3 are squares mod p which is why you don't even need QR for the cases I originally mentioned

#### Mario Carneiro (Apr 02 2021 at 08:23):

I would be remiss to not mention the proof of dirichlet's theorem in the form "every arithmetic progression contains infintely many primes" done in lean by translation from metamath. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336

#### Mario Carneiro (Apr 02 2021 at 08:25):

It's not in mathlib, though, because it has a dependency on the metamath library

Last updated: May 17 2021 at 15:13 UTC