English
For all natural numbers a,b, the condition (∀ p, ordCompl_p(a) | ordCompl_p(b)) is equivalent to a | b.
Русский
Для всех a,b: (∀ p, ordCompl_p(a) | ordCompl_p(b)) эквивалентно a | b.
LaTeX
$$$$ \forall a,b \in \mathbb{N},\ (\forall p, \operatorname{ordCompl}_{p}(a) \mid \operatorname{ordCompl}_{p}(b)) \iff a \mid b. $$$$
Lean4
theorem ordCompl_dvd_ordCompl_iff_dvd (a b : ℕ) : (∀ p : ℕ, ordCompl[p] a ∣ ordCompl[p] b) ↔ a ∣ b :=
by
refine ⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩
rcases eq_or_ne b 0 with (rfl | hb0)
· simp
if pa : a.Prime then ?_ else simpa [pa] using h a
if pb : b.Prime then ?_ else simpa [pb] using h b
rw [prime_dvd_prime_iff_eq pa pb]
by_contra hab
apply pa.ne_one
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]
simpa [Prime.factorization_self pb, Prime.factorization pa, hab] using h b
