x,y:
, n:
. ((x
y) mod n) = mod_guard((x mod n)(y mod n);n)x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n)| Rank | Theorem | Name |
| 8 | Thm* x,y:, n:. ((xy) mod n) = mod_guard((x mod n)(y mod n);n) | [mod_mul_guard] |
| cites | ||
| 7 | Thm* x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n) | [mod_mul] |