Galois Theory

Shinji KONO ([email protected]), University of the Ryukyus

Galois Theory

Symmetric.agda       symmetic group
Solvable.agda        commutator and solvable 

Gutil.agda           lemma on a group 
Putil.agda           lemma on Permutation
fin.agda             lemma on Data.Fin
logic.agda           lemma on Logic
nat.agda             lemma on Data.Nat

sym2.agda            Symmetric 2 is solvable
sym3.agda            Symmetric 3 is solvable
sym4.agda            Symmetric 4 is solvable
sym5.agda            Symmetric 5 is not solvable

FLutil.agda          unique concrete representation of Permutation
                     with Fresh List
FLComm.agda          Solvable in FL / FList

sym2n.agda           proved by Any
sym3n.agda           
sym4n.agda           
sym5n.agda           command line computation for compile

Todo : some proofs in FLutil / FLComm are not finished

we cannot remove --warning=noUnsupportedIndexedMatch from lib because of FLutil / Fresh List