a,b,n:
. (n
gcd(a;b)) ~ gcd(na;nb)a,b,y1,y2:. GCD(a;b;y1) 
GCD(a;b;y2) (y1 ~ y2)a,b,y,n:. GCD(a;b;y) GCD(na;nb;ny)| Rank | Theorem | Name |
| 5 | a,b,n:. (ngcd(a;b)) ~ gcd(na;nb) | [gcd_mul] |
| cites the following: | ||
| 0 | a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2) | [gcd_unique] |
| 4 | a,b,y,n:. GCD(a;b;y) GCD(na;nb;ny) | [gcd_p_mul] |