English
For a prime p and x with x ≤ p^n but not ≤ p^{n+1}, the multiplicity of p in the normalized factors of x is exactly n.
Русский
При простом p и x с x ≤ p^n, но не ≤ p^{n+1}, кратность p в нормализованных факторах x равна n.
LaTeX
$$count_normalizedFactors_eq$$
Lean4
theorem mul_mem_pow (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : ℕ} (h : a * b ∈ I ^ n) : a ∈ I ∨ b ∈ I ^ n :=
by
cases n; · simp
by_cases hI0 : I = ⊥; · simpa [pow_succ, hI0] using h
simp only [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq, ← Ideal.dvd_iff_le,
← Ideal.span_singleton_mul_span_singleton] at h ⊢
by_cases ha : I ∣ span { a }
· exact Or.inl ha
rw [mul_comm] at h
exact Or.inr (Prime.pow_dvd_of_dvd_mul_right ((Ideal.prime_iff_isPrime hI0).mpr hI) _ ha h)
