Extracting weighted prime powers from a pair of integers

Call a pair of integers (A, B) primitive of weight (m, n) if no prime ℓ has both ℓ ^ m ∣ A and ℓ ^ n ∣ B. For positive weights, every pair not both zero is (d ^ m * A', d ^ n * B') for a nonzero integer d and a pair (A', B') primitive of weight (m, n): stripping one prime at a time strictly decreases |A| + |B|. For weight (1, 1) this is the extraction of a greatest common divisor, as in Int.exists_gcd_one; for weight (4, 6) it produces the minimal-pair short Weierstrass equation y² = x³ + Ax + B of an elliptic curve over ℚ, where (A, B) ↦ (u⁴A, u⁶B) is the coefficient freedom of a short equation.

Main results

• Int.exists_eq_pow_mul_and_forall_prime_not_pow_dvd_of_ne_zero: the statement above.

theorem Int.exists_eq_pow_mul_and_forall_prime_not_pow_dvd_of_ne_zero (A B : ℤ) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (h : A ≠ 0 ∨ B ≠ 0) : ∃ (d : ℤ), ∃ (A' : ℤ), ∃ (B' : ℤ), d ≠ 0 ∧ A = d ^ m * A' ∧ B = d ^ n * B' ∧ ∀ (ℓ : ℕ), Nat.Prime ℓ → ¬(↑ℓ ^ m ∣ A' ∧ ↑ℓ ^ n ∣ B')

Every pair of integers, not both zero, is a weighted power times a primitive pair: for positive weights m and n there are d ≠ 0 and A', B' with A = d ^ m * A', B = d ^ n * B', and no prime ℓ with both ℓ ^ m ∣ A' and ℓ ^ n ∣ B'.