English
Auxiliary lemma showing the finite-sets case follows from the general product-of-prime-powers CRT.
Русский
Лемма-вспомогатель показывает, что частный случай для конечного множества следует из общего CRT по простым степеням.
LaTeX
$$Eq (s.prod (P_i^{e_i})) I → Eq (Finset.univ.prod (P_i^{e_i})) I$$
Lean4
/-- The bijection between the set of prime factors of the ideal `⟨r⟩` and the set of prime factors
of `r` preserves `count` of the corresponding multisets. See
`multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity` for the version
stated in terms of multiplicity. -/
theorem count_span_normalizedFactors_eq {r X : R} (hr : r ≠ 0) (hX : Prime X) :
Multiset.count (Ideal.span { X } : Ideal R) (normalizedFactors (Ideal.span { r })) =
Multiset.count (normalize X) (normalizedFactors r) :=
by
have := emultiplicity_eq_emultiplicity_span (R := R) (a := X) (b := r)
rw [emultiplicity_eq_count_normalizedFactors (Prime.irreducible hX) hr,
emultiplicity_eq_count_normalizedFactors (Prime.irreducible ?_), normalize_apply, normUnit_eq_one, Units.val_one,
one_eq_top, mul_top, Nat.cast_inj] at this
· simp only [normalize_apply, this]
· simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, hr, not_false_eq_true]
· simpa only [prime_span_singleton_iff]
