English
Let p be irreducible with normalize(p) = p. If p^n | x and p^{n+1} ∤ x, then the count of p in normalizedFactors(x) equals n.
Русский
Пусть p ирредуцируемо и normalize(p)=p. Если p^n делит x, а p^{n+1} не делит x, то количество p в normalizedFactors(x) равно n.
LaTeX
$$$\\text{Irreducible } p \\Rightarrow \\text{normalizedFactors}(x)\\text{ count}_p = n \\text{ under } p^n \\mid x \\land \\lnot p^{n+1} \\mid x.$$$
Lean4
/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`.
See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
-/
theorem count_normalizedFactors_eq [DecidableEq R] {p x : R} (hp : Irreducible p) (hnorm : normalize p = p) {n : ℕ}
(hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : (normalizedFactors x).count p = n := by
classical
by_cases hx0 : x = 0
· simp [hx0] at hlt
apply Nat.cast_injective (R := ℕ∞)
convert (emultiplicity_eq_count_normalizedFactors hp hx0).symm
· exact hnorm.symm
exact (emultiplicity_eq_coe.mpr ⟨hle, hlt⟩).symm
