English
For p,q in a Euclidean domain with q ≠ 0, the elements p/gcd(p,q) and q/gcd(p,q) are coprime. This captures the standard normalized coprimality after dividing by their gcd.
Русский
Для p,q в евклидовом домене с q ≠ 0 элементы p/gcd(p,q) и q/gcd(p,q) взаимно просты. Это отражает нормализованную взаимную простоту после деления на gcd.
LaTeX
$$$\\text{IsCoprime}(p/\\gcd(p,q),\\ q/\\gcd(p,q))$ при q ≠ 0$$
Lean4
theorem isCoprime_div_gcd_div_gcd (hq : 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' (gcd_ne_zero_of_right hq) <| gcd_dvd_left _ _).symm
(EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_right _ _).symm <|
gcd_ne_zero_of_right hq
