x,y:
, n:
. ((x
y) mod n) = (((x mod n)(y mod n)) mod n)a:, n:. a = (a 
n)n+(a mod n) & (a mod n) < na:, n:, q:, r:. a = qn+r 
r < n q = (a n) & r = (a mod n)| Rank | Theorem | Name |
| 7 | Thm* x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n) | [mod_mul] |
| cites | ||
| 2 | Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n | [div_floor_mod_properties] |
| 6 | Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) | [div_floor_mod_unique] |