English
One of the standard lemmas relating emultiplicities across factorizations and divisor relations.
Русский
Один из стандартных лемм, связывающих эмп множества через разложение и делители.
LaTeX
$$emultiplicity (span{P_i^{e_i}}) (span{P_j^{e_j}}) = emultiplicity (P_i^{e_i}) (P_j^{e_j})$$
Lean4
/-- The bijection `normalizedFactorsEquivSpanNormalizedFactors` between the set of prime
factors of `r` and the set of prime factors of the ideal `⟨r⟩` preserves multiplicities. See
`count_normalizedFactorsSpan_eq_count` for the version stated in terms of multisets `count`. -/
theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity {r d : R} (hr : r ≠ 0)
(hd : d ∈ normalizedFactors r) :
emultiplicity d r =
emultiplicity (normalizedFactorsEquivSpanNormalizedFactors hr ⟨d, hd⟩ : Ideal R) (Ideal.span { r }) :=
by
simp only [normalizedFactorsEquivSpanNormalizedFactors, emultiplicity_eq_emultiplicity_span, Subtype.coe_mk,
Equiv.ofBijective_apply]
