Mercurial > hg > Members > kono > Proof > galois
view README.md @ 302:3812936d52c8
remove lift
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 07 Sep 2023 11:45:11 +0900 |
parents | a5b3061f15ee |
children |
line wrap: on
line source
Galois Theory ============ Shinji KONO (kono@ie.u-ryukyu.ac.jp), 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