n:
. 0<n 
(q,r:. nmod(q
n+r;n) = nmod(r;n))Thm* (
n:hnum. implies
Thm* (
n:hnum. (lt(0,n)
Thm* (
n:hnum. ,all
Thm* (
n:hnum. ,(q:hnum. all
Thm* (
n:hnum. ,(q:hnum. (r:hnum. equal(mod(add(mult(q,n),r),n),mod(r,n))))))| Theorem | Name |
| n:. 0<n (q,r:. nmod(qn+r;n) = nmod(r;n)) | [mod_times] |
| cites the following: | |
Thm* ( n:hnum. implies
Thm* ( n:hnum. (lt(0,n)
Thm* ( n:hnum. ,all
Thm* ( n:hnum. ,(q:hnum. all
Thm* ( n:hnum. ,(q:hnum. (r:hnum. equal(mod(add(mult(q,n),r),n),mod(r,n)))))) | [hmod_times] |