Theorem Ideal.multiplicity_span_eq_multiplicity

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.multiplicity_span_eq_multiplicityView on Github →