English
If a and b are coprime and n is a prime power, then n divides a·b if and only if n divides a or n divides b.
Русский
Пусть a и b взаимно просты, а n — степень простого. Тогда n делит произведение a·b тогда и только тогда, когда n делит a или n делит b.
LaTeX
$$$(\gcd(a,b)=1) \wedge \operatorname{IsPrimePow}(n) \Rightarrow (n \mid ab \iff n \mid a \lor n \mid b)$$$
Lean4
theorem isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.Coprime a b) (hn : IsPrimePow n) : n ∣ a * b ↔ n ∣ a ∨ n ∣ b :=
by
rcases eq_or_ne a 0 with (rfl | ha)
· simp
rcases eq_or_ne b 0 with (rfl | hb)
· simp
refine
⟨?_, fun h =>
Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a))) fun i =>
i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply, Finsupp.coe_add]
have : a.factorization p = 0 ∨ b.factorization p = 0 :=
by
rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ← Finset.mem_inter]
intro t
simpa using hab.disjoint_primeFactors.le_bot t
rcases this with h | h <;> simp [h, imp_or]
