English
Let p be prime. For all n, q divides p^n iff there exists i ≤ n with q associated to p^i.
Русский
Пусть p — простое. Для каждого n верно: q делит p^n тогда и только тогда, когда существует i ≤ n, такое что q ассоциировано с p^i.
LaTeX
$$q \mid p^n \iff \exists i \le n,\ Associated(q, p^i)$$
Lean4
theorem dvd_prime_pow [CancelCommMonoidWithZero M] {p q : M} (hp : Prime p) (n : ℕ) :
q ∣ p ^ n ↔ ∃ i ≤ n, Associated q (p ^ i) := by
induction n generalizing q with
| zero => simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]
| succ n ih =>
refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
rw [pow_succ'] at h
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)
· rw [mul_dvd_mul_iff_left hp.ne_zero, ih] at h
rcases h with ⟨i, hi, hq⟩
refine ⟨i + 1, Nat.succ_le_succ hi, (hq.mul_left p).trans ?_⟩
rw [pow_succ']
· obtain ⟨i, hi, hq⟩ := ih.mp hno
exact ⟨i, hi.trans n.le_succ, hq⟩
