a:
, n:
. mod_guard(a;n) 
a
a rem n ;((-a) rem n)=00 else n-((-a) rem n) fia:, n:. (a mod n) == {i:| 0 < i } Type| Some definitions of interest. | |
| mod_guard | Def mod_guard(x;y) == x mod y |
| Thm* a:, n:. mod_guard(a;n) | |
| modulus | Def a mod n == if 0aa rem n ;((-a) rem n)=00 else n-((-a) rem n) fi |
| Thm* a:, n:. (a mod n) | |
| nat_plus | Def == {i:| 0 < i } |
| Thm* Type |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |