English
If gcd(p,q) ≠ 0 in a Euclidean domain, then p/gcd(p,q) and q/gcd(p,q) are coprime. This is a variant that replaces a distinct nonzero assumption with gcd(p,q) ≠ 0.
Русский
Если gcd(p,q) ≠ 0 в евклидовом домене, то p/gcd(p,q) и q/gcd(p,q) взаимно просты. Это версия, которая заменяет дополнительное неравенство условия на gcd(p,q) ≠ 0.
LaTeX
$$$\\text{IsCoprime}(p/\\gcd(p,q), q/\\gcd(p,q)) $ при gcd(p,q) ≠ 0$$
Lean4
/-- This is a version of `isCoprime_div_gcd_div_gcd` which replaces the `q ≠ 0` assumption with
`gcd p q ≠ 0`. -/
theorem isCoprime_div_gcd_div_gcd_of_gcd_ne_zero (hpq : GCDMonoid.gcd p q ≠ 0) :
IsCoprime (p / GCDMonoid.gcd p q) (q / GCDMonoid.gcd p q) :=
(gcd_isUnit_iff _ _).1 <|
isUnit_gcd_of_eq_mul_gcd (EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_left _ _).symm
(EuclideanDomain.mul_div_cancel' (hpq) <| gcd_dvd_right _ _).symm <|
hpq
