Ssreflect Users Discussion List

[Georges Gonthier <>]

  On second thought, the suggested construction might not work that well, 
because roots of the cyclotomic polynomial might fail to be primitive in 
prime characteristic (the GCD of Phi with X^d - 1 might be divisible by the 
characteristic). One must use the fact that X^(p^m) - X is separable in 
characteristic p.
Perhaps it will be easier to forget about primitive roots, carve out F_{p^m} 
as the subfield of roots of X^(p^m) - X in the algebraic closure of F_p 
(which you can get from countalg.v), and use separable_prod_XsubC to show 
that the subfield has exactly p^m elements.
    Sorry,
Georges

-----Original Message-----
From:  
[] On Behalf Of Georges Gonthier
Sent: 18 September 2014 13:40
To: Strub, Pierre-Yves; 
Subject: RE: [ssreflect] Galois fields

   Hi Pierre-Yves,

Indeed, 'F_p is $F_p$ if p is prime, and $F_2$ otherwise.  Apart from the 
fact that we need to use F_p way before we could ever construct F_{p^m}, an 
important feature of this definition if that arithmetic in 'F_p is 
convertible to arithmetic modulo a prime (equal to p if p is prime); that 
couldn't be the case if it were just a special case of the more general 
construction...
   Unfortunately for you, we never quite got around to actually constructing 
the finite fields in the development: in the Odd Order proof they arise 
explicitly as sections of our hypothetical counter-example. However, it 
should be straightforward to construct them from the bits that are there:
   - field extensions (falgebra/filedext.v), especially theorem irredp_FAdjoin
   - cyclotomic polynomials (cyclotomic.v) You'll need to extend the results 
in cyclotomic, to show that any root of an image of 'Phi_n is a primitive 
m-th root of unity (I only did this for the image in C).
Then:
  + get an irreducible factor of the image of 'Phi_(p^m-1)  (e.g., rVpoly 
[arg min_(v < (poly_rV P : 'rV_(size P)| rVpoly v %| P) size (rVpoly p)], 
where P := map_poly inZp 'Phi_(p ^ m - 1), using mxpoly functions).
  + use irredp_FAdjoin to construct 'F_{p ^ m} (the syntax I had in mind) as 
an extension of F_p with a primitive (p^m - 1)-th root of unity omega.
  + 'F_{p ^ m} will have at least p^m elements (0 + the powers of omega), but 
by the Frobenius automorphism all are roots of  'X^(p ^m) - 'X, so there are 
exactly p^m of them.

    Best,
Georges

-----Original Message-----
From:  
[] On Behalf Of Strub, Pierre-Yves
Sent: 16 September 2014 18:41
To: 
Subject: [ssreflect] Galois fields

Hi,

I thought for a long time that 'F_p was constructing F_(q^n) where q is the 
smallest prime dividing p and n is its power in the prime decomposition of p. 
Where can I find such a construction? I expect to have something close to 
what I want in the Galois formalization of ssr, but I'm not (yet) used to 
that part.

Cheers,
-- Pierre-Yves.