count_pow — Mathlib

English

If a ≠ 0 and for every irreducible p, k divides p.count a.factors, then there exists b with a = b^k.

Русский

Если a ≠ 0 и для каждого неприводимого p число k делит p.count a.factors, то существует b такое, что a = b^k.

LaTeX

$$$$a \\neq 0 \\Rightarrow (\\forall p, \\mathrm{Irreducible}(p) \\Rightarrow k \\mid \\mathrm{count}(p,a.factors)) \\Rightarrow \\exists b:\\; a = b^k.$$$$

Lean4

theorem count_pow [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) :
    count p (a ^ k).factors = k * count p a.factors := by
  induction k with
  | zero => rw [pow_zero, factors_one, zero_mul, count_zero hp]
  | succ n h => rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]; ring

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