dvd_count_pow — Mathlib

English

For nonzero a, and irreducible p, the divisor count of p^k in a^k equals k times the divisor count in a.

Русский

Для не нулевого a и неприводимого p число делителей p^k в разложении a^k равно k умножить на число делителей p в a.

LaTeX

$$$$a \\neq 0 \\land \\mathrm{Irreducible}(p) \\\\Rightarrow k \\mid \\mathrm{count}(p,(a^k).factors).$$$$

Lean4

theorem dvd_count_pow [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) :
    k ∣ count p (a ^ k).factors := by
  rw [count_pow ha hp]
  apply dvd_mul_right

Похожие утверждения