HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Finite fields (Galois fields) #2007

Open Alizter opened 3 months ago

Alizter commented 3 months ago

We should define finite fields as they form useful examples of rings.

We have cyclic groups of order n so it should be enough to take a prime and define the usual multiplication.

We don't yet have material on prime numbers so I'll create an issue for that too.

As for prime powers, we will probably need things like splitting fields which is a bit non-trivial for the moment.