The prime powers that decide whether a divisor fits beside a fixed factor

Let f and d both divide h. Whether the product f * d still divides h is decided one prime at a time, and only at the primes of f: room for f * d fails at p exactly when d carries p to a power that exceeds the room h leaves after f, which is v_p h - v_p f. So f * d ∣ h holds exactly when no prime p of f divides d to the exponent v_p h - v_p f + 1.

The one-sided reading is what makes the statement useful: the primes outside f impose no condition, because d ∣ h already leaves them enough room.

The exponents v_p h - v_p f + 1 are themselves exponents of prime powers dividing h, both one prime at a time and all at once, since the primes of f are distinct.

Main results

• Nat.mul_dvd_iff_forall_not_pow_dvd: f * d ∣ h as non-divisibility of d by a prime power at each prime of f.
• Nat.pow_factorization_sub_factorization_add_one_dvd: the tested prime power divides h.
• Nat.prod_pow_factorization_sub_factorization_add_one_dvd: so does their product over the primes of f.

theorem Nat.mul_dvd_iff_forall_not_pow_dvd {f d h : ℕ} (hh : h ≠ 0) (hf : f ∣ h) (hd : d ∣ h) : f * d ∣ h ↔ ∀ p ∈ f.primeFactors, ¬p ^ (h.factorization p - f.factorization p + 1) ∣ d

A divisor fits beside a fixed factor exactly away from prime powers. For f and d dividing a nonzero h, the product f * d divides h if and only if no prime p of f divides d to the exponent v_p h - v_p f + 1.

Only the primes of f are tested: at a prime p not dividing f the hypothesis d ∣ h already gives v_p d ≤ v_p h.

theorem Nat.pow_factorization_sub_factorization_add_one_dvd {f h : ℕ} (hf : f ∣ h) {p : ℕ} (hp : p ∈ f.primeFactors) : p ^ (h.factorization p - f.factorization p + 1) ∣ h

The prime power tested by mul_dvd_iff_forall_not_pow_dvd divides h. For f dividing h and p a prime of f, the exponent v_p h - v_p f + 1 does not exceed v_p h, because f contributes at least one power of p.

theorem Nat.prod_pow_factorization_sub_factorization_add_one_dvd {f h : ℕ} (hf : f ∣ h) : ∏ p ∈ f.primeFactors, p ^ (h.factorization p - f.factorization p + 1) ∣ h

The product of the prime powers tested by mul_dvd_iff_forall_not_pow_dvd divides h. The primes of f are distinct, so the prime powers p ^ (v_p h - v_p f + 1) occur at distinct primes and their product still divides h: it is the product of prime powers read off a finitely supported exponent function bounded by the factorization of h.