English
Let hp be irreducible p and a|p^n. Then a = p^{Nat.find (fun n => a ∣ p^n) ⟨n,h⟩}. This expresses a as a pure p-power with exponent equal to the least exponent making a divide p^n.
Русский
Пусть hp ирредуцируемый p; если a делится на p^n, то a = p^{Nat.find (λ t, a ∣ p^t) ⟨n,h⟩}. Это выражает, что a — степенная на p с показателем, равным наименьшему n, при котором a делится на p^n.
LaTeX
$$$\\forall a\\ p,\\ hp : Irreducible\\ p\\Rightarrow \\forall {n}, (a \\mid p^n) \\Rightarrow a = p^{\\operatorname{Nat.find}(\\,\\lambda t, a \\mid p^t\\,)\\langle n,h\\rangle}$$$
Lean4
/-- The only divisors of prime powers are prime powers. -/
theorem eq_pow_find_of_dvd_irreducible_pow {a p : Associates α} (hp : Irreducible p) [∀ n : ℕ, Decidable (a ∣ p ^ n)]
{n : ℕ} (h : a ∣ p ^ n) : a = p ^ @Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩ :=
by
classical rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]
exact h
