Mercurial > hg > Members > kono > Proof > galois

changeset 128:206fc12e5c36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 05 Sep 2020 10:34:53 +0900
parents 43d00372bdc9
children dae027341d73
files README.md
diffstat 1 files changed, 12 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/README.md	Sat Sep 05 08:59:57 2020 +0900
+++ b/README.md	Sat Sep 05 10:34:53 2020 +0900
@@ -9,15 +9,19 @@
 Symmetric.agda       symmetic group
 Solvable.agda        commutator and solvable 
 
-Gutil.agda
-Putil.agda
-fin.agda
-logic.agda
-nat.agda
+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
-sym3.agda
-sym5.agda
+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.