coq-galois-theory

A formalization of the Fundamental Theorem of Galois Theory in the Coq proof assistant

We attempt to prove the famous theorem of Galois of abstract algebra giving the relationship between fixed fields of certain field isomorphisms and subgroups of the Galois group of such isomorphisms.