Disjointness of the combined gcd/D-only part from the E-only part
Provedgpy_primeFactors_gcd_disjoint_rightnumber-theory
For squarefree D and E, the prime divisors of gcd D E together with those of D / gcd D E are disjoint from the prime divisors of E / gcd D E. This is an unconditional elementary lemma.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_primeFactors_gcd_disjoint_right {D E : ℕ} (hsqD : Squarefree D)
(hsqE : Squarefree E) :
Disjoint ((Nat.gcd D E).primeFactors ∪ (D / Nat.gcd D E).primeFactors)
(E / Nat.gcd D E).primeFactors := by sorrySource
GPY monomial joint (GPYMonomialJoint.lean), restated into Mathlib-only terms