annotate README.md @ 284:69645d667f45

rename
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Jan 2023 11:40:29 +0900 (2023-01-29)
parents a5b3061f15ee
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 Galois Theory
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 ============
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 ## Galois Theory
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 ```
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 Symmetric.agda symmetic group
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 Solvable.agda commutator and solvable
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
128
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
12 Gutil.agda lemma on a group
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
13 Putil.agda lemma on Permutation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
14 fin.agda lemma on Data.Fin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
15 logic.agda lemma on Logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
16 nat.agda lemma on Data.Nat
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
128
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
18 sym2.agda Symmetric 2 is solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
19 sym3.agda Symmetric 3 is solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
20 sym4.agda Symmetric 4 is solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
21 sym5.agda Symmetric 5 is not solvable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
22
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
23 FLutil.agda unique concrete representation of Permutation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
24 with Fresh List
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
25 FLComm.agda Solvable in FL / FList
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
26
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
27 sym2n.agda proved by Any
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
28 sym3n.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
29 sym4n.agda
254
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
30 sym5n.agda command line computation for compile
72
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 ```
09fa2ab75703 add utilties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 128
diff changeset
34 Todo : some proofs in FLutil / FLComm are not finished