a
a rem n ;((-a) rem n)=00 else n-((-a) rem n) fi
a:
, n:
. (a mod n) 
j == if i=j true ; false fii,j:. (i=j) 
j == 
j < ii,j:. (ij) j == if i < j true ; false fii,j:. (i < j) b == if b false else true fib:. b | Who Cites modulus? | |
| 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) | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) | |
| le_int | Def ij == j < i |
| Thm* i,j:. (ij) | |
| lt_int | Def i < j == if i < j true ; false fi |
| Thm* i,j:. (i < j) | |
| bnot | Def b == if b false else true fi |
| Thm* b:. b |
| Syntax: | a mod n | has structure: | modulus(a; n) |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |