English
Definition of a finite-collection Chinese remainder isomorphism realizing R/I as a product over a finite index set.
Русский
Определение конечного CRT-изоморфизма, реализующего R/I как произведение по конечному индексу.
LaTeX
$$quotientEquivPiOfFinsetProdEq {I} {P} {e} ...$$
Lean4
/-- The bijection `normalized_factors_equiv_span_normalized_factors.symm` between the set of prime
factors of the ideal `⟨r⟩` and the set of prime factors of `r` preserves multiplicities. -/
theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity {r : R} (hr : r ≠ 0)
(I : {I : Ideal R | I ∈ normalizedFactors (Ideal.span ({ r } : Set R))}) :
emultiplicity ((normalizedFactorsEquivSpanNormalizedFactors hr).symm I : R) r =
emultiplicity (I : Ideal R) (Ideal.span { r }) :=
by
obtain ⟨x, hx⟩ := (normalizedFactorsEquivSpanNormalizedFactors hr).surjective I
obtain ⟨a, ha⟩ := x
rw [hx.symm, Equiv.symm_apply_apply, Subtype.coe_mk,
emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity hr ha]
