Mercurial > hg > Members > kono > Proof > galois
view README.md @ 136:5689c06be30d
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 08 Sep 2020 13:51:10 +0900 |
parents | 206fc12e5c36 |
children | 59d12d02dfa8 |
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 ``` Todo : Use Data.List.Fresh to obtain all list of FL, and Commutator of FL. It should make sym2, sym3 and sym4 simpler.