Theorem Ideal.emultiplicity_span_eq_emultiplicity

Modification history

2026-09-07 13:44
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(RingTheory/Ideal): generalize span_singleton_dvd_span_singleton_iff_dvd and emultiplicity_eq_emultiplicity_span (#40557) …
Added Ideal.emultiplicity_span_eq_emultiplicityView on Github →