x:
, n:
. (n | x) 
(x mod n) = 0x,y:, n:. ((x
y) mod n) = mod_guard((x mod n)(y mod n);n)x,y:, n:. ((x+y) mod n) = mod_guard((x mod n)+(y mod n);n)
a
a rem n ;((-a) rem n)=00 else n-((-a) rem n) fi
is mentioned by
| Thm* x:, n:. (n | x) (x mod n) = 0 | [elim_divides] |
| Thm* x,y:, n:. ((xy) mod n) = mod_guard((x mod n)(y mod n);n) | [mod_mul_guard] |
| Thm* x,y:, n:. ((x+y) mod n) = mod_guard((x mod n)+(y mod n);n) | [mod_add_guard] |
| Def mod_guard(x;y) == x mod y | [mod_guard] |
In prior sections: int 2 graph 1 1
Try larger context:
Graphs