|
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
|
|
72
|
23
|
|
|
24 ```
|
|
|
25
|
|
128
|
26 Todo : Use Data.List.Fresh to obtain all list of FL, and Commutator of FL.
|
|
|
27 It should make sym2, sym3 and sym4 simpler.
|
