English
Let hp be irreducible p. For every n, if a divides p^n, then the least such exponent equals p.count a.factors, i.e., Nat.find (fun n => a | p^n) ⟨n,h⟩ = p.count a.factors.
Русский
Пусть hp — ирредуцируемый p. Для любого n, если a делится на p^n, наименьшая такая экспонента равна p.count a.factors, то есть Nat.find (λ n, a | p^n) ⟨n, h⟩ = p.count a.factors.
LaTeX
$$$\\text{hp irreducible} \\Rightarrow \\forall {n}, (a \\mid p^n) \\Rightarrow \\operatorname{Nat.find}(\\,\\lambda t, a \\mid p^t\\,)(\\langle n,h\\rangle) = p.count\\, a.factors$$$
Lean4
theorem count_factors_eq_find_of_dvd_pow {a p : Associates α} (hp : Irreducible p) [∀ n : ℕ, Decidable (a ∣ p ^ n)]
{n : ℕ} (h : a ∣ p ^ n) : @Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩ = p.count a.factors :=
by
apply le_antisymm
· refine Nat.find_le ⟨1, ?_⟩
rw [mul_one]
symm
exact eq_pow_count_factors_of_dvd_pow hp h
· have hph := pow_ne_zero (@Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩) hp.ne_zero
rcases subsingleton_or_nontrivial α with hα | hα
· simp [eq_iff_true_of_subsingleton] at hph
convert count_le_count_of_le hph hp (@Nat.find_spec (fun n => a ∣ p ^ n) _ ⟨n, h⟩)
rw [count_pow hp.ne_zero hp, count_self hp, mul_one]
