n:
. 0<n 
(k:. nmod(k
n;n) = 0)
n:hnum. implies(lt(0,n),all(k:hnum. equal(mod(mult(k,n),n),0))))| Theorem | Name |
| n:. 0<n (k:. nmod(kn;n) = 0) | [mod_eq_0] |
| cites the following: | |
| n:hnum. implies(lt(0,n),all(k:hnum. equal(mod(mult(k,n),n),0)))) | [hmod_eq_0] |