PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: mod mul guard
x,y:, n:. ((xy) mod n) = mod_guard((x mod n)(y mod n);n)
By:
Auto
THEN
Unfold `mod_guard` 0
THEN
BackThru Thm* x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n)
Generated subgoals:

None

About:
intmultiplyequalall

PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc