Part of claim 2

[metakunt]

I have added parts of claim 2 to the database. I have found the following theorem which shall be useful to us.
https://us.metamath.org/mpeuni/fta1g.html

Essentially, given a set A and a non-zero polynomial P if every element of A is a root of P, then the degree of P is an upper bound of the size of A.

Thus it appears that we have to show that the algebraic closure of Galois fields are integral domains. We likely will need to show that they are fields anyway, so we are able to apply the lemma above.

I am not quite sure how far we need to have Galois closures and even if we need them. What do you think about it?

[metakunt]

Also this corresponds to https://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf Lemma 4.8 which is much cleaner written.

[metakunt]

I think this reduces the computation in $$F_p$$ to the computation in $$\mathbb{Z}_p/(X^r-1)$$ and we may have more tools here already.