Step * of Lemma gcd_mul

∀a,b,n:ℤ.  ((n * gcd(a;b)) ~ gcd(n * a;n * b))
BY
{ Auto }

1
1. a : ℤ
2. b : ℤ
3. n : ℤ
⊢ (n * gcd(a;b)) ~ gcd(n * a;n * b)


Latex:


Latex:
\mforall{}a,b,n:\mBbbZ{}.    ((n  *  gcd(a;b))  \msim{}  gcd(n  *  a;n  *  b))


By


Latex:
Auto




Home Index