Commit 2026-09-07 13:44 bf0ef6d9

feat(RingTheory/Ideal): generalize span_singleton_dvd_span_singleton_iff_dvd and emultiplicity_eq_emultiplicity_span (#40557) Move Ideal.span_singleton_dvd_span_singleton_iff_dvd from Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas to Mathlib.RingTheory.Ideal.Operations. The result holds for any CommSemiring — the [IsPrincipalIdealRing R] hypothesis was not needed. Generalize Ideal.emultiplicity_eq_emultiplicity_span from [IsDomain R] [IsPrincipalIdealRing R] to [CommRing R]. The proof simplifies considerably: it follows immediately from emultiplicity_eq_emultiplicity_iff and the generalized dvd lemma. :robot: This PR was extracted from the SKW project by Claude.