Invitation to construction of finite fields

[Meta Kunt]

­Now that my construction out of Zn[X]/(X^r-1) to a field K with characteristic dividing n with a r-th primitive root is complete all that's left to prove the following statement.

 

exfinfield $p |- A. p e. Prime A. n e. NN E. k e. Field ( # ` ( Base ` k ) ) = ( p ^ n ) $= ? $.

I have looked at the proof in mathlib and I am trying to understand what we need to prove the theorem. The main idea is the following.
We start by adjoining a single root of an irreducible polynomial. This gives us a F_p algebra and a field, which we can extend by adjoining all monic divisors of X^(p^n)-X.
This set is finite and it is ordered, since Z/nZ and Z/nZ[X] is totally ordered, thus we can take the minimal element without choice.

The construction gives us a field, but we need to show that it is a splitting field. There are some facts that we will need to develop. First, all elements of x satisfy x^(p^n)-x = 0, and by the gcd argument there are no multiple roots.

I'd propose to work a little bit like I did with primitive roots. Have an axiomatic symbol for splitting field that only holds the axioms and then prove properties for splitting fields abstractly instead of working with a specific construction like https://us.metamath.org/mpeuni/df-sfl.html.

I've ported the following theorems.
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#IsPrimitiveRoot.pow_ne_one_of_pos_of_lt corresponds to https://us.metamath.org/mpeuni/primrootlekpowne0.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#IsPrimitiveRoot.coe_units_iff corresponds to https://us.metamath.org/mpeuni/primrootsunit.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#IsPrimitiveRoot.pow_of_coprime correpsonds https://us.metamath.org/mpeuni/primrootscoprmpow.html 

https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.html#IsPrimitiveRoot.pow_eq_one_iff_dvd corresponds to https://us.metamath.org/mpeuni/primrootspoweq0.html

In principle we wouldn't need the full API, just enough to prove the results of interest.


Thus I want to know who would be interested in collaborating. If there is sufficient interest I'd really research the complete construction and write a detailed blueprint of what we need to prove to get the construction working.
 

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.