Primes in the form 6n ± 1

Stream: mathlib4

[Kajani Kaunda]

Hello, has the following known result been formalized and added to mathlib?: every prime ≥ 3 can be expressed in the form 6n ± 1.

[Johan Commelin]

I don't think it is in mathlib. But it makes for a nice exercise.

[Yury G. Kudryashov]

Please include a version assuming Nat.Coprime n 6 instead of Nat.Prime n and n > 3 in your PR if you're going to make it.

[Yury G. Kudryashov]

(or should we assume that n is an odd number and 3 doesn't divide n?)

[Kajani Kaunda]

Yury G. Kudryashov said:

Please include a version assuming Nat.Coprime n 6 instead of Nat.Prime n and n > 3 in your PR if you're going to make it.

A co-prime version is certainly interesting. And n can be even I guess since 6x4 -1 is prime, ...

[Kajani Kaunda]

Johan Commelin said:

I don't think it is in mathlib. But it makes for a nice exercise.

It certainly does. It's amazing how many interesting use-cases of this result!

[Yury G. Kudryashov]

I meant a lemma saying that for every n such that Nat.Coprime n 6 we have n = 6k ± 1 for some k.

[Kajani Kaunda]

Yury G. Kudryashov said:

I meant a lemma saying that for every n such that Nat.Coprime n 6 we have n = 6k ± 1 for some k.

Ah! ok!

[Yury G. Kudryashov]

Or you can assume Odd n and ¬(3 ∣ n) instead of Nat.Coprime n 6.

[Yury G. Kudryashov]

Then you apply this theorem for a prime number p.

[Kajani Kaunda]

Yury G. Kudryashov said:

Or you can assume Odd n and ¬(3 ∣ n) instead of Nat.Coprime n 6.

One way or the other, its a must-have in MathLib.

[Kajani Kaunda]

Forgive me I am not a trained mathematician, my background is Computer Science but I am finding the line between the two is getting thinner! I am also new to LEAN and this community but I am SUPER motivated to get up to speed in Math and LEAN.... :smile:

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

Sorry I misread your question

[Something Something]

might also want to include p^2 = 1 mod 24

[Something Something]

and also might want to do it for every mod primorial
https://en.wikipedia.org/wiki/Primorial

[Kajani Kaunda]

Something Something said:

and also might want to do it for every mod primorial
https://en.wikipedia.org/wiki/Primorial

Mmmm, interesting point! Perhaps if one wants to use a result like 6n ± 1, one may just have to prove and use it in ones work rather than seek to have it in MATHLIB which might unnecessarily end up bloating MATHLIB up! What do you think? Is that a reasonable conclusion?

[Yury G. Kudryashov]

It depends on how often this particular result appears in the proofs.

[Yury G. Kudryashov]

We have lots of trivial lemmas in Mathlib.

[Kajani Kaunda]

Yury G. Kudryashov said:

We have lots of trivial lemmas in Mathlib.

Ah, ok!

[Kajani Kaunda]

Anyway, I will give it a try. As previously noted, it is a good exercise. I will share results once I succeed. If I get stuck, I will not hesitate to ask for help, The community is very helpful. I am thankful for that!