Mercurial > hg > Papers > 2020 > kono-prosym
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"/>