Defining a set of primes and their additive inverses

Stream: lean4

[Kajani Kaunda]

What would be the LEAN4 code to define the following;

the set J = (..., -p$$_{n+2}$$, -p$$_{n+1}$$, -p$$_n$$, p$$_n$$, p$$_{n+1}$$, p$$_{n+2}$$, ...) which would give us: J = (..., -5, -3, -2, 2, 3, 5, ...).

Note: the elements of the set J are all the primes and their additive inverses.
I would like to be able to test it on the site: https://live.lean-lang.org/

[Kajani Kaunda]

Kajani Kaunda said:

What would be the LEAN4 code to define the following;

the set J = (..., -p$$_{n+2}$$, -p$$_{n+1}$$, -p$$_n$$, p$$_n$$, p$$_{n+1}$$, p$$_{n+2}$$, ...) which would give us: J = (..., -5, -3, -2, 2, 3, 5, ...).

Note: the elements of the set J are all the primes and their additive inverses.
I would like to be able to test it on the site: https://live.lean-lang.org/

Oops!, I did not get the subscripts right! sorry!

[Yaël Dillies]

What about

import Mathlib

#check {n : ℤ | Prime n}

[Kajani Kaunda]

Yaël Dillies said:

What about

import Mathlib

#check {n : ℤ | Prime n}

Does that include the additive inverses...

[Yaël Dillies]

Yes it does. Prime numbers in the integers correspond to prime numbers in the natural numbers and their negations

[Kajani Kaunda]

Yaël Dillies said:

Yes it does. Prime numbers in the integers correspond to prime numbers in the natural numbers and their negations

Ah , Ok!

[Yaël Dillies]

example : -2 ∈ {n : ℤ | Prime n} := Int.prime_two.neg

[Kajani Kaunda]

Yaël Dillies said:

example : -2 ∈ {n : ℤ | Prime n} := Int.prime_two.neg

Thank you!