NameDateSize

..09-Nov-20206

files.txtH A D09-Nov-20201.3 KiB

helperScript.smlH A D09-Nov-202032.8 KiB

HolmakefileH A D09-Nov-2020235

involuteActionScript.smlH A D09-Nov-202024.7 KiB

involuteFixScript.smlH A D09-Nov-202045.3 KiB

involuteScript.smlH A D09-Nov-20208.1 KiB

iterateComposeScript.smlH A D09-Nov-202071.4 KiB

iterateComputeScript.smlH A D09-Nov-202038.6 KiB

iterateScript.smlH A D09-Nov-202037 KiB

README.mdH A D09-Nov-2020770

twoSquaresScript.smlH A D09-Nov-202052.9 KiB

windmillScript.smlH A D09-Nov-202065.8 KiB

README.md

1
2# Fermat's Two Squares Theorem, with an algorithm.
3
4These scripts contain theories to support the formalisation of an algorithm for Fermat's Two Squares Theorem.
5
6## Theory
7* __helper__, helper theorems for arithmetic, sets, maps and lists.
8* __involute__, basic properties of involution.
9* __involuteFix__, pairs and fixes of involution.
10* __involuteAction__, involution and group action.
11* __iterate__, iteration of a function, with period of iteration.
12* __iterateCompose__, iteration of involution composition.
13* __iterateCompute__, iteration period computation, recursion and while-loop.
14
15## Application
16* __windmill__, definitions of windmill, mill, flip, and zaiger.
17* __twoSquares__, existence, uniqueness and algorithm of two squares theorem.
18