English
The emultiplicity between principal ideals equals the emultiplicity between their generators.
Русский
Эмпиричность между двумя главными идеалами равна эмпитичности между их генераторами.
LaTeX
$$emultiplicity(span{a}, span{b}) = emultiplicity(a, b)$$
Lean4
theorem emultiplicity_eq_emultiplicity_span {a b : R} :
emultiplicity (Ideal.span { a }) (Ideal.span ({ b } : Set R)) = emultiplicity a b :=
by
by_cases h : FiniteMultiplicity a b
· rw [h.emultiplicity_eq_multiplicity]
apply emultiplicity_eq_of_dvd_of_not_dvd <;>
rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
· exact pow_multiplicity_dvd a b
· apply h.not_pow_dvd_of_multiplicity_lt
apply lt_add_one
· suffices ¬FiniteMultiplicity (Ideal.span ({ a } : Set R)) (Ideal.span ({ b } : Set R)) by
rw [emultiplicity_eq_top.2 h, emultiplicity_eq_top.2 this]
exact
FiniteMultiplicity.not_iff_forall.mpr fun n =>
by
rw [Ideal.span_singleton_pow, span_singleton_dvd_span_singleton_iff_dvd]
exact FiniteMultiplicity.not_iff_forall.mp h n
