English
If p equals 0 or p is irreducible and normalize p = p, then the count in normalizedFactors x equals n under the usual divisibility conditions.
Русский
Если p = 0 или p неразложимо и normalize p = p, тогда при данных условиях делимости count в normalizedFactors x равен n.
LaTeX
$$$\text{If } p = 0 \text{ or } Irreducible(p) \text{ and } normalize(p) = p, \text{ then } (normalizedFactors x).count p = n$$$
Lean4
/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`. This is a slightly more general version of
`UniqueFactorizationMonoid.count_normalizedFactors_eq` that allows `p = 0`.
See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
-/
theorem count_normalizedFactors_eq' [DecidableEq R] {p x : R} (hp : p = 0 ∨ Irreducible p) (hnorm : normalize p = p)
{n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : (normalizedFactors x).count p = n :=
by
rcases hp with (rfl | hp)
· cases n
· exact count_eq_zero.2 (zero_notMem_normalizedFactors _)
· rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt
exact absurd hle hlt
· exact count_normalizedFactors_eq hp hnorm hle hlt
