Complete Integers in Agda

Project information

In this work we will define a superset of integers (the complete integers), which contains the dual of integers along parity (e.g. the odd zero, the even one, ...). Then we will see how they form a ring and how they can be used as exponents for real numbers powers, in order to write functions which have a discontinuity in zero (the function itself or one of its derivates), as for example the absolute value and the sign function.

Agda algebra integers

+ 1 more

53 Commits
2 Branches
0 Tags

README
GitLab Pages

Created on

May 09, 2022

Copy SSH clone URLgit@gitlab.com:DPDmancul/complete-integers-agda.git
Copy HTTPS clone URLhttps://gitlab.com/DPDmancul/complete-integers-agda.git