English
Let p be prime. For every n, if p ∤ a and p^n ∣ a b, then p^n ∣ b.
Русский
Пусть p простое. Для каждого n, если p не делит a и p^n делит a b, то p^n делит b.
LaTeX
$$$\\text{Prime}(p) \\Rightarrow \\forall n:\\, \\mathbb{N},\\; (p \\nmid a) \\land (p^n \\mid a b) \\Rightarrow p^n \\mid b.$$$
Lean4
theorem pow_dvd_of_dvd_mul_left [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ a)
(h' : p ^ n ∣ a * b) : p ^ n ∣ b := by
induction n with
| zero =>
rw [pow_zero]
exact one_dvd b
| succ n ih =>
obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
rw [pow_succ]
apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
