English
The number of times I occurs as a normalized factor of J is the same as the coefficient of J in the factorization of I, counted up to associates.
Русский
Число вхождений I как нормализованного фактора в J равно коэффициенту J в факторизации I с учётом ассоциирования.
LaTeX
$$count_associates_factors_eq$$
Lean4
/-- The number of times an ideal `I` occurs as normalized factor of another ideal `J` is stable
when regarding these ideals as associated elements of the monoid of ideals. -/
theorem count_associates_factors_eq [DecidableEq (Ideal R)] [DecidableEq <| Associates (Ideal R)]
[∀ (p : Associates <| Ideal R), Decidable (Irreducible p)] {I J : Ideal R} (hI : I ≠ 0) (hJ : J.IsPrime)
(hJ₀ : J ≠ ⊥) : (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I) :=
by
replace hI : Associates.mk I ≠ 0 := Associates.mk_ne_zero.mpr hI
have hJ' : Irreducible (Associates.mk J) := by
simpa only [Associates.irreducible_mk] using (Ideal.prime_of_isPrime hJ₀ hJ).irreducible
apply (Ideal.count_normalizedFactors_eq (p := J) (x := I) _ _).symm
all_goals
rw [← Ideal.dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
simp only [Associates.dvd_eq_le]
rw [Associates.prime_pow_dvd_iff_le hI hJ']
cutsat
