|
72
|
1 Galois Theory
|
|
|
2 ============
|
|
|
3
|
|
|
4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
|
|
|
5
|
|
|
6 ## Galois Theory
|
|
|
7
|
|
|
8 ```
|
|
|
9 Symmetric.agda symmetic group
|
|
|
10 Solvable.agda commutator and solvable
|
|
|
11
|
|
128
|
12 Gutil.agda lemma on a group
|
|
|
13 Putil.agda lemma on Permutation
|
|
|
14 fin.agda lemma on Data.Fin
|
|
|
15 logic.agda lemma on Logic
|
|
|
16 nat.agda lemma on Data.Nat
|
|
72
|
17
|
|
128
|
18 sym2.agda Symmetric 2 is solvable
|
|
|
19 sym3.agda Symmetric 3 is solvable
|
|
|
20 sym4.agda Symmetric 4 is solvable
|
|
|
21 sym5.agda Symmetric 5 is not solvable
|
|
|
22
|
|
184
|
23 FLutil.agda unique concrete representation of Permutation
|
|
|
24 with Fresh List
|
|
|
25 FLComm.agda Solvable in FL / FList
|
|
|
26
|
|
|
27 sym2n.agda proved by Any
|
|
|
28 sym3n.agda
|
|
|
29 sym4n.agda
|
|
72
|
30
|
|
|
31 ```
|
|
|
32
|
|
184
|
33 Todo : some proofs in FLutil / FLComm are not finished
|
