diff Galois1.mm @ 4:353edf5ef2d9

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Jan 2021 09:43:12 +0900
parents 57601db306e9
children
line wrap: on
line diff
--- a/Galois1.mm	Thu Jan 07 13:28:35 2021 +0900
+++ b/Galois1.mm	Sat Jan 09 09:43:12 2021 +0900
@@ -212,12 +212,15 @@
 </node>
 <node TEXT="solvable" ID="ID_178918488" CREATED="1609990354030" MODIFIED="1609990359075"/>
 </node>
-<node TEXT="symmetric group representation in agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1609990393339">
+<node TEXT="symmetric groupin agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1610005855100">
+<node TEXT="representation" ID="ID_319391779" CREATED="1610005856583" MODIFIED="1610005864458">
 <node TEXT="Data.Fin" ID="ID_1340949296" CREATED="1609990393883" MODIFIED="1609990404918"/>
 <node TEXT="Bijection" ID="ID_316860227" CREATED="1609990405535" MODIFIED="1609990409631"/>
 <node TEXT="List" ID="ID_1710126935" CREATED="1609990410154" MODIFIED="1609990413645"/>
 <node TEXT="FL" ID="ID_235104633" CREATED="1609990415278" MODIFIED="1609990419436"/>
 </node>
+<node TEXT="1 to 1" ID="ID_1677442759" CREATED="1610005903688" MODIFIED="1610005907592"/>
+</node>
 <node TEXT="proofs" ID="ID_1219242238" CREATED="1609992596012" MODIFIED="1609992600251">
 <node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_514245484" CREATED="1609992600706" MODIFIED="1609992602407"/>
 <node TEXT="injection" ID="ID_1366306030" CREATED="1609992603682" MODIFIED="1609992607205">
@@ -232,6 +235,10 @@
 <node TEXT="a list contains everything" ID="ID_67235294" CREATED="1609990709190" MODIFIED="1609990733750">
 <node TEXT="sorted" ID="ID_73107613" CREATED="1609990734279" MODIFIED="1609990738112"/>
 <node TEXT="any" ID="ID_1569296473" CREATED="1609990738656" MODIFIED="1609990745411"/>
+<node TEXT="enumeration" ID="ID_992373663" CREATED="1610005876529" MODIFIED="1610005884864">
+<node TEXT="permutation" ID="ID_535994" CREATED="1610005972212" MODIFIED="1610005978496"/>
+<node TEXT="commutator" ID="ID_1725495702" CREATED="1610005979019" MODIFIED="1610005984240"/>
+</node>
 </node>
 <node TEXT="Fresh List" ID="ID_928929976" CREATED="1609990754285" MODIFIED="1609990759712">
 <node TEXT="Set valued function" ID="ID_1431257568" CREATED="1609990760342" MODIFIED="1609990767070"/>
@@ -242,6 +249,7 @@
 </node>
 <node TEXT="insert" ID="ID_1479901665" CREATED="1609990795810" MODIFIED="1609990799803"/>
 <node TEXT="insert / cons and Any" ID="ID_265930485" CREATED="1609990800355" MODIFIED="1609990813411"/>
+<node TEXT="enumeration of pair" ID="ID_622029876" CREATED="1610006179353" MODIFIED="1610006194627"/>
 </node>
 <node TEXT="proofs" ID="ID_71982613" CREATED="1609990838839" MODIFIED="1609990843748">
 <node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_1357773799" CREATED="1609990844233" MODIFIED="1609990848197"/>