n:
. 0<n 
(k:. nmod(nmod(k;n);n) = nmod(k;n))Thm* (
n:hnum. implies(lt(0,n),all(k:hnum. equal(mod(mod(k,n),n),mod(k,n)))))| Theorem | Name |
| n:. 0<n (k:. nmod(nmod(k;n);n) = nmod(k;n)) | [mod_mod] |
| cites the following: | |
Thm* ( n:hnum. implies(lt(0,n),all(k:hnum. equal(mod(mod(k,n),n),mod(k,n))))) | [hmod_mod] |