## Stream: math-comp users

### Topic: ✔ Definition of the set of Prime numbers.

#### Jannik Mähn (May 31 2024 at 10:49):

Thanks you two for you help! The final solution looks like this:

``````From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

Variable n : nat.

Definition P := [set x : 'I_n.+1 | prime x].

Lemma four_notin_P : inZp 4 \notin P.
Proof.

End Primes.
``````

#### Notification Bot (May 31 2024 at 10:49):

Jannik Mähn has marked this topic as resolved.

#### Bas Spitters (May 31 2024 at 14:01):

@Jannik Mähn I was going to point to the coq-prima package, but now I see there are actually a number of packages defining them: https://github.com/thery/coqprime
https://coq.inria.fr/coq-package-index (search prime-numbers).

#### Jannik Mähn (Jun 05 2024 at 14:23):

Thanks Bas, I'll have a look there as well!

#### Jannik Mähn (Jun 13 2024 at 09:52):

Dear math-comp users, I have to reopen the topic.

How can we define a type for the set of primes that we have defined above?

So, given this definition:

``````From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

Variable n : nat.
Definition P := [set x : 'I_n.+1 | prime x].

End Primes.
``````

We need to write something like this:

``````From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

Variable n : nat.
Definition P' : {set x : 'I_n.+1 | prime x} := [set x : 'I_n.+1 | prime x].

End Primes.
``````

Where I get a syntax error right now.

There might also be another approach, where we define things like this:

``````From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

Variable n : nat.

Definition P : {set 'I_n.+1} := [set : 'I_n.+1].
Parameter all_prime : forall x, x \in P -> prime x.
Definition Z_n_prod := [finType of P].

End Primes.
``````

I want to define it in this
`finType`
notation becauce of the setting we're working in. Here I get the following error:

``````**Error:** `The term "P" has type "{set 'I_n.+1}" while it is expected to have type "Type".`
``````