English
If a divides b, then ordCompl_p(a) divides ordCompl_p(b) for every p.
Русский
Если a делит b, то ordCompl_p(a) делит ordCompl_p(b) для каждого p.
LaTeX
$$$$ a \mid b \Rightarrow \operatorname{ordCompl}_{p}(a) \mid \operatorname{ordCompl}_{p}(b). $$$$
Lean4
theorem ordCompl_dvd_ordCompl_of_dvd {a b : ℕ} (hab : a ∣ b) (p : ℕ) : ordCompl[p] a ∣ ordCompl[p] b :=
by
rcases em' p.Prime with (pp | pp)
· simp [pp, hab]
rcases eq_or_ne b 0 with (rfl | hb0)
· simp
rcases eq_or_ne a 0 with (rfl | ha0)
· cases hb0 (zero_dvd_iff.1 hab)
have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'
have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'
rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]
intro q
rcases eq_or_ne q p with (rfl | hqp)
· simp
simp_rw [erase_ne hqp]
exact (factorization_le_iff_dvd ha0 hb0).2 hab q
