English
The multiplicity of a normalized factor is preserved under the quotient equivalence.
Русский
Величина кратности нормального делителя сохраняется под эквивалентностью квоти.
LaTeX
$$normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity$$
Lean4
theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors (hJ : J ≠ ⊥) {L : Ideal R}
(hL : L ∈ normalizedFactors I) :
↑(idealFactorsEquivOfQuotEquiv f ⟨L, dvd_of_mem_normalizedFactors hL⟩) ∈ normalizedFactors J :=
by
have hI : I ≠ ⊥ := by
intro hI
rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
exact Finset.notMem_empty _ hL
refine
mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL (d :=
(idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
rintro ⟨l, hl⟩ ⟨l', hl'⟩
rw [Subtype.coe_mk, Subtype.coe_mk]
apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f
