Disjointness of the gcd part and the D-only part for squarefree D
Provedgpy_primeFactors_gcd_disjoint_leftnumber-theory
For squarefree D, the prime divisors of gcd D E are disjoint from the prime divisors of D / gcd D E: a common prime would square-divide D. This is an unconditional elementary lemma.
Preamble
import Mathlib open Classical
Formal statement
theorem gpy_primeFactors_gcd_disjoint_left {D E : ℕ} (hsqD : Squarefree D) :
Disjoint (Nat.gcd D E).primeFactors (D / Nat.gcd D E).primeFactors := by sorrySource
GPY monomial joint (GPYMonomialJoint.lean), restated into Mathlib-only terms